From: Lutz Donnerhacke <lutz@iks-jena.de>
Subject: Re: [Spark] Some Linux tools
Date: Mon, 24 Mar 2003 14:08:39 +0000 (UTC)
Date: 2003-03-24T14:08:39+00:00 [thread overview]
Message-ID: <slrnb7u4b3.o1.lutz@taranis.iks-jena.de> (raw)
In-Reply-To: slrnb7mhmi.nu.lutz@taranis.iks-jena.de
* Lutz Donnerhacke wrote:
> 1) If using the standard Spark tools, it's not that refreshing to wait on a
> somewhat slower machine for the results ... To have a look is more
> interesting.
>
> 2) Sometimes the simplifier can not solve all trivial problems. There might
> be a very simple hint to guide the simplifier to the right result. But
> in order to do so, the *.rls files has to be changed, before the simplifier
> can run.
>
> 3) In order to provide the examiner access to the necessary sources, a simple
> way is using an index file. This should be easily generated.
>
> ftp://ftp.iks-jena.de/pub/mitarb/lutz/ada/spark/ contains two files:
> rules.pl replacement of sparksimp working on 1) and 2)
> spark_update_index.pl working on 3) (errornous, take with grain)
I replaced the rules.pl by sparksimp.pl.
Of course, this program does not require 12MB stack space like pogs.
If you need other outputs, please mail me.
$ sparksimp.pl --help
Usage: sparksimp.pl [rulefile]
Searches for all unsimplified 'vcg' files, modifies the 'rls' file, if
necessary, invokes the simplifier, and generate a pogs like statistics report.
The rulefile may consists of additional rules for examiner generated rule
families. Every rule set starts with a comma seperated list of target families
followed by the space indented rules themself. The following example was the
reason to introduce this feature:
kill_group_rules, kill_all_rules:
- X <= Y may_be_replaced_by X >= - Y.
- X >= Y may_be_replaced_by X <= - Y.
$ sparksimp.pl kernel.rul
Switching to .
Adding directory kernel_
Switching to kernel_
Adding directory io
Adding directory processes
Switching to io
permission_to_string: Testing ... reading ... simplifying
[A two line progess indicator is shown here:
First line: procedure/function currently simplified with proof counter.
Second line: Last line of the spadesimp stdout log.]
permission_to_string: Collecting statistics ... vcg, siv ... done
mode_to_string: Testing ... reading ... simplifying
mode_to_string: Collecting statistics ... vcg, siv ... done
string_to_fullpath: Testing ... reading ... simplifying
string_to_fullpath: Collecting statistics ... vcg, siv ... done
mkdir: Testing ... reading ... simplifying
mkdir: Collecting statistics ... vcg, siv ... done
rename: Testing ... reading ... simplifying
rename: Collecting statistics ... vcg, siv ... done
getdents_empty: Testing ... reading ... simplifying
getdents_read: Collecting statistics ... vcg, siv ... done
getdents: Testing ... reading ... simplifying
getdents: Collecting statistics ... vcg, siv ... done
Switching back
Switching to processes
kill_all: Testing ... done
kill_all: Collecting statistics ... vcg, siv ... done
kill_process: Testing ... done
kill_process: Collecting statistics ... vcg, siv ... done
kill_my_group: Testing ... done
kill_my_group: Collecting statistics ... vcg, siv ... done
kill_group: Testing ... done
kill_group: Collecting statistics ... vcg, siv ... done
Switching back
Switching back
Writing statistics ... done
$ cat kernel.sum
-------------------------------------------------------------------------------
Semantic Analysis Summary
-------------------------------------------------------------------------------
Summary of:
Verification Condition files (.vcg)
Simplified Verification Condition files (.siv)
in the directory: /var/home/lutz/work/ada/src/kernel
VCs for kernel_/processes/kill_process
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 26 | YES |
2 | start | rtc check @ 26 | YES |
3 | start | rtc check @ 26 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 140 | YES |
2 | start | rtc check @ 141 | YES |
3 | start | rtc check @ 143 | YES |
4 | start | rtc check @ 145 | YES |
5 | start | finish | YES |
6 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/mode_to_string
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 60 | YES |
2 | start | rtc check @ 67 | YES |
3 | start | rtc check @ 68 | YES |
4 | start | assert @ 71 | YES |
5 | start | assert @ 71 | YES |
6 | start | assert @ 71 | YES |
7 | assert @ 71 | rtc check @ 73 | YES |
8 | assert @ 71 | rtc check @ 74 | YES |
9 | assert @ 71 | assert @ 77 | YES |
10 | assert @ 71 | assert @ 77 | YES |
11 | assert @ 71 | assert @ 77 | YES |
12 | assert @ 77 | rtc check @ 79 | YES |
13 | assert @ 77 | rtc check @ 80 | YES |
14 | assert @ 77 | assert @ 83 | YES |
15 | assert @ 77 | assert @ 83 | YES |
16 | assert @ 77 | assert @ 83 | YES |
17 | assert @ 83 | rtc check @ 85 | YES |
18 | assert @ 83 | rtc check @ 86 | YES |
19 | assert @ 83 | rtc check @ 87 | YES |
20 | assert @ 83 | rtc check @ 88 | YES |
21 | assert @ 83 | rtc check @ 89 | YES |
22 | assert @ 83 | rtc check @ 90 | YES |
23 | assert @ 83 | rtc check @ 91 | YES |
24 | assert @ 83 | finish | YES |
25 | assert @ 83 | finish | YES |
26 | assert @ 83 | finish | YES |
27 | assert @ 83 | finish | YES |
28 | assert @ 83 | finish | YES |
29 | assert @ 83 | finish | YES |
30 | assert @ 83 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_my_group
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 33 | YES |
2 | start | rtc check @ 33 | YES |
3 | start | rtc check @ 33 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents_empty
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents_read
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 185 | YES |
2 | start | rtc check @ 186 | YES |
3 | start | rtc check @ 190 | YES |
4 | start | rtc check @ 191 | YES |
5 | start | rtc check @ 194 | YES |
6 | start | rtc check @ 195 | YES |
7 | start | rtc check @ 196 | YES |
8 | start | rtc check @ 197 | YES |
9 | start | rtc check @ 197 | YES |
10 | start | assert @ 197 | YES |
11 | assert @ 197 | assert @ 197 | YES |
12 | assert @ 197 | rtc check @ 200 | YES |
13 | assert @ 197 | rtc check @ 201 | YES |
14 | start | rtc check @ 208 | YES |
15 | start | rtc check @ 208 | YES |
16 | assert @ 197 | rtc check @ 208 | YES |
17 | assert @ 197 | rtc check @ 208 | YES |
18 | start | finish | YES |
19 | start | finish | YES |
20 | start | finish | YES |
21 | start | finish | YES |
22 | assert @ 197 | finish | YES |
23 | assert @ 197 | finish | YES |
24 | assert @ 197 | finish | YES |
25 | assert @ 197 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/permission_to_string
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 18 | YES |
2 | start | rtc check @ 19 | YES |
3 | start | rtc check @ 19 | YES |
4 | start | rtc check @ 20 | YES |
5 | start | rtc check @ 20 | YES |
6 | start | rtc check @ 20 | YES |
7 | start | rtc check @ 20 | YES |
8 | start | finish | YES |
9 | start | finish | YES |
10 | start | finish | YES |
11 | start | finish | YES |
12 | start | finish | YES |
13 | start | finish | YES |
14 | start | finish | YES |
15 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_group
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 40 | YES |
2 | start | rtc check @ 41 | YES |
3 | start | rtc check @ 42 | YES |
4 | start | rtc check @ 42 | YES |
5 | start | rtc check @ 42 | YES |
6 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/mkdir
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 241 | YES |
2 | start | rtc check @ 241 | YES |
3 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/string_to_fullpath
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 99 | YES |
2 | start | assert @ 99 | YES |
3 | assert @ 99 | assert @ 99 | YES |
4 | assert @ 99 | rtc check @ 102 | YES |
5 | start | rtc check @ 104 | YES |
6 | assert @ 99 | rtc check @ 104 | YES |
7 | start | finish | YES |
8 | assert @ 99 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_all
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 20 | YES |
2 | start | rtc check @ 20 | YES |
3 | start | rtc check @ 20 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/rename
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 249 | YES |
2 | start | rtc check @ 249 | YES |
3 | start | finish | YES |
-------------------------------------------------------------------------------
\f===============================================================================
--------------- Proved By --------------
Total Examiner Simplifier Checker Review Undischarged
Assert 13 0 13 0 0 0
Postcondition 34 34 0 0 0 0
Runtime check 62 0 62 0 0 0
===============================================================================
Totals 109 34 75 0 0 0
% Totals 31% 68% 0% 0% 0%
===================== End of Semantic Analysis Summary ========================
next prev parent reply other threads:[~2003-03-24 14:08 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-21 17:07 [Spark] Some Linux tools Lutz Donnerhacke
2003-03-24 14:08 ` Lutz Donnerhacke [this message]
2003-03-27 18:03 ` Rod Chapman
2003-03-28 11:47 ` Lutz Donnerhacke
2003-03-28 15:27 ` Lutz Donnerhacke
2003-03-31 17:25 ` Stephen Leake
2003-04-01 8:14 ` Lutz Donnerhacke
2003-04-01 8:38 ` Jacob Sparre Andersen
2003-04-01 9:18 ` Adrian Knoth
2003-04-08 13:46 ` Rod Chapman
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox