From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,9741d8c9cef792de X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-24 06:08:41 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail From: Lutz Donnerhacke Newsgroups: comp.lang.ada Subject: Re: [Spark] Some Linux tools Date: Mon, 24 Mar 2003 14:08:39 +0000 (UTC) Organization: IKS GmbH Jena Message-ID: References: NNTP-Posting-Host: taranis.iks-jena.de X-Trace: branwen.iks-jena.de 1048514919 741 217.17.192.37 (24 Mar 2003 14:08:39 GMT) X-Complaints-To: usenet@iks-jena.de NNTP-Posting-Date: Mon, 24 Mar 2003 14:08:39 +0000 (UTC) User-Agent: slrn/0.9.7.4 (Linux) Xref: archiver1.google.com comp.lang.ada:35648 Date: 2003-03-24T14:08:39+00:00 List-Id: * 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs for kernel_/io/getdents_empty ------------------------------------------------------------------------------- | | |--- Proved In --- | No | From | To | vcg siv plg prv TODO | ------------------------------------------------------------------------------- 1 | start | finish | YES | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- VCs 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 | ------------------------------------------------------------------------------- =============================================================================== --------------- 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 ========================