Jessie Tutorial (811290)
Текст из файла
Jessie Plugin TutorialFrama-C version: BoronJessie plugin version: 2.26Claude Marché1,3 , Yannick Moy2,3 ,May 31, 20101INRIA Saclay - Île-de-France, ProVal, Orsay, F-91893France Télécom, Lannion, F-223073LRI, Univ Paris-Sud, CNRS, Orsay, F-914052c2009-2010INRIAThis work was supported by the ‘CAT’ ANR project (ANR-05-RNTL-0030x) and by the ANR CIFRE contract2005/973.Contents1Introduction1.1 Batch Mode vs.
GUI Mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.2 Basic Use . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.3 Safety Checking vs. Functional Verification . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .22252Safety Checking2.1 Memory Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2 Integer Overflow Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3 Checking Termination . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . .889113Functional Verification3.1 Behaviors . . . . . . . . . . . . . . . . . . .3.1.1 Simple functional property . . . . . .3.1.2 More advanced functional properties .3.2 Advanced Algebraic Modeling . . . . .
. . .....13131313154Inference of Annotations4.1 Postconditions and Loop Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.2 Preconditions and Loop Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1818185Separation of Memory Regions206Treatment of Unions and Casts227Reference Manual7.1 General usage . . . . . . . . . . .
. . . .7.2 Unsupported features . . . . . . . . . . .7.2.1 Unsupported C features . . . . . .7.2.2 partially supported ACSL features7.2.3 Unsupported ACSL features . . .7.3 Command-line options . . . . . . . . . .7.4 Pragmas . . . . . . . . . . . . . . . . . ..........................1.....................................................................................................................................................................................................................................................................................................2424242425252526Chapter 1Introduction1.1Batch Mode vs.
GUI ModeThe Jessie plug-in allows to perform deductive verification of C programs inside Frama-C. The C file possiblyannotated in ACSL is first checked for syntax errors by Frama-C core, before it is translated to various intermediatelanguages inside the Why Platform embedded in Frama-C, and finally verification conditions (VC) are generatedand a prover is called on these, as sketched in Figure 1.1.By default, the Jessie plug-in launches the GUI mode. To invoke this mode on a file ex.c, just type> frama-c -jessie ex.cThe GUI of the Why Plaform (a.k.a. GWhy) is called.
It presents each VC on a line, with available provers oncolumns.To invoke the plug-in in batch mode, use the -jessie-atp with the prover name as argument, e.g.> frama-c -jessie -jessie-atp simplify ex.cruns the prover Simplify on the generated VCs. Valid identifiers for provers are documented in Why, it includesalt-ergo, cvc3, yices, z3. See also the prover tricks page http://why.lri.fr/provers.html.Finally, you can use the generic name goals to just ask for generation of VCs without running any prover.1.2Basic UseA program does not need to be complete nor annotated to be analyzed with the Jessie plug-in.
As a first example,take program max:int max(int i, int j) {return (i < j) ? j : i;}Calling the Jessie plug-in in batch mode generates the following output:frama-c -jessie -jessie-atp simplify max.cParsing[preprocessing] running gcc -C -E -I. -include/usr/local/share/frama-c/jessie/jessie_prolog.h -dD max.cCleaning unused partsSymbolic linkStarting semantical analysisStarting Jessie translationProducing Jessie files in subdir max.jessieFile max.jessie/max.jc written.File max.jessie/max.cloc written.Calling Jessie tool in subdir max.jessie2Figure 1.1: Frama-C and the Why PlatformGenerating Why function fCalling VCs generator.why -simplify [...] why/max.whyRunning Simplify on proof obligations(.
= valid * = invalid ? = unknown # = timeout ! = failure)simplify/max_why.sx: (0/0/0/0/0)The result of calling prover Simplify is succinctly reported as a sequence of symbols ., *, ?, # and ! whichdenote respectively that the corresponding VC is valid, invalid or unknown, or else that a timeout or a failureoccured. By default, timeout is set to 10 s for each VC. This result is summarized as a tuple (v,i,u,t,f) reporting thetotal number of each outcome.Here, summary (0/0/0/0/0) says that there were no VC to prove.
If instead we call the Jessie plug-inin GUI mode, we get no VC to prove. Indeed, function max is safe and we did not ask for the verification of afunctional property.Consider now adding a postcondition to function max://@ ensures \result == ((i < j) ? j : i);int max(int i, int j) {return (i < j) ? j : i;}This ACSL annotation expresses the fact function max returns the maximum of its parameters i and j.
Now,running the Jessie plug-in in batch mode outputs:3...Running Simplify on proof obligations(. = valid * = invalid ? = unknown # = timeout ! = failure)simplify/max_why.sx: .? (1/0/1/0/0)total:2valid:1 ( 50%)invalid :0 ( 0%)unknown :1 ( 50%)timeout :0 ( 0%)failure :0 ( 0%)total wallclock time : 0.19 sectotal CPU time: 0.16 secvalid VCs:average CPU time : 0.08max CPU time: 0.08invalid VCs:average CPU time : nanmax CPU time: 0.00unknown VCs:average CPU time : 0.08max CPU time: 0.08This says that Simplify could prove one VC and not the other. To see what these VC represent, we call now theJessie plug-in in GUI mode. Each VC represents verification of the postcondition in a different context.
The firstVC represents the context where i < j:The second VC represents the context where i >= j. Context can be seen in the upper right panel of GWhy,expressed in the intermediate language of Why. It is not yet possible to retrieve the equivalent C expressions orstatements.Running Simplify inside GWhy shows that the second VC is not proved by Simplify. However, it is proved byprover Alt-Ergo.4The Jessie plug-in can also be run in batch mode with prover Alt-Ergo instead of Simplify, with option-jessie-atp alt-ergo, which results in the following output:...Running Alt-Ergo on proof obligations(. = valid * = invalid ? = unknown # = timeout ! = failure)why/max_why.why: .. (2/0/0/0/0)total:2valid:2 (100%)invalid :0 ( 0%)unknown :0 ( 0%)timeout :0 ( 0%)failure :0 ( 0%)total wallclock time : 0.35 sectotal CPU time: 0.14 secvalid VCs:average CPU time : 0.07max CPU time: 0.08invalid VCs:average CPU time : nanmax CPU time: 0.00unknown VCs:average CPU time : nanmax CPU time: 0.001.3Safety Checking vs.
Functional VerificationIn the simple max example, VC for the postcondition are grouped in the default behavior for function max. Ingeneral, VC for a function are grouped in more than one group:• Safety: VC this group guard against safety violations such as null-pointer dereferencing, buffer overflow,integer overflow, etc.• Default behavior: VC in this group concern the verification of a function’s default behavior, which includesverification of its postcondition, frame condition, loop invariants and intermediate assertions.• User-defined behavior: VC in this group concern the verification of a function’s user-defined behavior,which includes verification of its postcondition, frame condition, loop invariants and intermediate assertionsfor this specific behavior.Here is a more complex variant of function max which takes pointer parameters and returns 0 on success and-1 on failure./*@@@@requires \valid(i) && \valid(j);requires r == \null || \valid(r);assigns *r;behavior zero:5@assumes r == \null;@assigns \nothing;@ensures \result == −1;@ behavior normal:@assumes \valid(r);@assigns *r;@ensures *r == ((*i < *j) ? *j : *i);@ensures \result == 0;@*/int max(int *r, int* i, int* j) {if (!r) return −1;*r = (*i < *j) ? *j : *i;return 0;}Notice that the annotations refer to the null pointer using ACSL syntax \null.
It would be possible to use alsothe C macro NULL, but in that case we would have to ask Frama-C preprocessor phase to process the annotationstoo, since it does not by default. This is done by option -pp-annot of Frama-C. However, this alternative is notrecommended since it is depended of the proprecessor in use (see http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start#faq_tips_and_tricks)Running the Jessie plug-in in GUI mode results in 4 groups of VC: Safety, Default behavior, Normal behavior‘normal‘ and Normal behavior ‘zero‘ for the two user-defined behaviors.6VC that are proved in one group can be available to prove VC in other groups. No circularity paradox ispossible here, since the proof of a VC can only rely on other VC higher in the control-flow graph of the function.We made the following choices:• To prove a VC in Safety, one can rely on VC in Default behavior.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
