Jessie Plugin

The Jessie pluginfor Deductive Verification in Frama-CTutorial and Reference ManualVersion 2.39Claude Marché, Yannick MoyAugust 23, 2017INRIA Team Toccata http://toccata.lri.frINRIA Saclay - Île-de-France & LRI, CNRS UMR 8623Batiment 650, Université Paris-Sud 91405 Orsay cedex, France2C. Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Contents1Introduction1.1 Important note for version 2.30 .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.2 Basic Use . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.3 Safety Checking vs. Functional Verification . . . . . . . . . . . . . . . . . . . . . . . .55562Safety Checking2.1 Memory Safety . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2 Integer Overflow Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3 Checking Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9911123Functional Verification3.1 Behaviors . .

. . . . . . . . . . . . . . . . .3.1.1 Simple functional property . . . . . .3.1.2 More advanced functional properties .3.2 Advanced Algebraic Modeling . . . . . . . .1313131315............................................................................................4Separation of Memory Regions195Reference Manual5.1 General usage . . . . .

. . . . . . . . . .5.2 Unsupported features . . . . . . . . . . .5.2.1 Unsupported C features . . . . . .5.2.2 partially supported ACSL features5.2.3 Unsupported ACSL features . . .5.3 Command-line options . . . . . . . . . .5.4 Pragmas . . . . . . . . . . . .

. . . . . .5.5 Troubleshooting . . . . . . . . . . . . . .212121212222232324........................................................................................................................................................................................................4C. Marché, Y. MoyCONTENTSWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Chapter 1IntroductionJessie is a plugin for the Frama-C environment, aimed at performing deductive verification of C programs, annotated using the ACSL language [4], using the Why [1] tool for generating proof obligations.This version 2.39 of Jessie is compatible with Frama-C version Nitrogen (and no other).1.1Important note for version 2.30The use of the Why2 VC generator is now obsolete, and it is recommended to switch to the Why3system for specification and VC generation.

Why3 must be installed independently of Why2, please seethe instructions given at http://why3.lri.fr.The version of Why3 that is compatible with this version 2.39 of Jessie is the version 0.71. Pleasesee http://krakatoa.lri.fr/ for more details on compatibility between Frama-C, Why2/Jessieand Why3.In this manual, it is assumed that the Why3 VC generator and IDE is in use. The old behavior usingthe Why2 VC generator and GUI remains possible, using option -jessie-atp=gui.1.2Basic UseThe Jessie plug-in allows to perform deductive verification of C programs inside Frama-C. The C filepossibly annotated in ACSL is first checked for syntax errors by Frama-C core, before it is translated tovarious intermediate languages inside the Why Platform embedded in Frama-C, and finally verificationconditions (VCs) are generated and a prover is called on these, as sketched in Figure 1.1.To prove the VCs generated, one needs to install external provers such as Alt-Ergo, CVC3 or Z3.Please see at URL http://krakatoa.lri.fr/ how to get such provers.

Once some of these areinstalled, you should run the auto-configuration tool by running command why3config -detect(equivalent to the former Why 2.xx command why-config)By default, the Jessie plug-in launches in its GUI mode. To invoke this mode on a file ex.c, justtype> frama-c -jessie ex.cA program does not need to be complete to be analyzed with the Jessie plug-in. As a first example,take program max://@ ensures \result == \max(i,j);int max(int i, int j) {return (i < j) ? j : i;}6IntroductionKML-annotatedJava programACSL-annotatedC programKrakatoaFrama-CJessieWhy 2.30VC generatorVC generatorTheoriesverificationconditionsverificationconditionsTransformationsEncodingsEncodingsWhy3 0.71Interactive provers(Coq, PVS,Isabelle/HOL, etc.)Automatic provers(Alt-Ergo, CVC3, Gappa,Simplify, veriT, Yices,Z3, etc.)More automatic provers(Eprover, SPASS,Vampire, etc.)Figure 1.1: Frama-C, the Why Platform and the new Why3 systemThe ACSL annotation expresses the fact function max returns the maximum of its parameters i and j.Now, running the Jessie plug-in launches Why3 IDE produces the output shown on Figure 1.2.On this figure, the user selected the row “WP Jessie program” and clicked on the buttons on the left,corresponding to provers Alt-Ergo, Z3 and CVC3.

The two VCs are shown valid, meaning that for thissmall function, the code matches its specification.1.3Safety Checking vs. Functional VerificationIn the simple max example, there are two VCs, one for the “default behavior” and one for “Safety” offunction max. In general, each function leads to these VCs:• Safety: this VC guard against safety violations such as null-pointer dereferencing, buffer overflow,integer overflow, etc.• Default behavior: this VC concern the verification of a function’s default behavior, which includesverification of its postcondition, frame condition, loop invariants and intermediate assertions.• User-defined behavior: these VCs concern the verification of a function’s user-defined behavior,which includes verification of its postcondition, frame condition, loop invariants and intermediateassertions for this specific behavior.Here is a more complex variant of function max which takes pointer parameters and returns 0 onsuccess and -1 on failure./*@ requires \valid(i) && \valid(j);C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20171.3 Safety Checking vs. Functional Verification7Figure 1.2: Why3 IDE for max function@ requires r == \null || \valid(r);@ assigns *r;@ behavior zero:@assumes r == \null;@assigns \nothing;@ensures \result == −1;@ behavior normal:@assumes \valid(r);@assigns *r;@ensures *r == \max(*i,*j);@ensures \result == 0;@*/int max(int *r, int* i, int* j) {C. Marché, Y.

MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20178IntroductionFigure 1.3: Why3 IDE for max_ptr functionif (!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 bepossible to use also the C macro NULL, but in that case we would have to ask Frama-C preprocessor phase to process the annotations too, since it does not by default. This is done by option -pp-annot of Frama-C. However, this alternative is not recommended since it depends of theproprecessor 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 VCs: Safety, default behavior, normal behavior‘normal‘ and normal behavior ‘zero‘ for the two user-defined behaviors.In the next chapters, we detail how to prove each kind of VC. We also recommend to look at thecollection of verified programs at URL http://toccata.lri.fr/gallery/jessieplugin.en.html to get more hints on how to specify and prove programs with Jessie.C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Chapter 2Safety CheckingA preliminary to the verification of functional properties using the Jessie plug-in is to verify the safetyof functions. Safety has several components: memory safety, integer safety, termination. Memory safetydeals with validity of memory accesses to allocated memory. Integer safety deals with absence of integeroverflows and validity of operations on integers, such as the absence of division by zero. Terminationamounts to check whether loops are always terminating, as well as recursive or mutually recursive functions.2.1Memory SafetyOur running example will be the famous binary_search function, which searches for a long in anordered array of longs.

On success, it returns the index at which the element appears in the array. Onfailure, it returns -1.#pragma JessieIntegerModel(math)#pragma JessieTerminationPolicy(user)int binary_search(long t[], int n, long v) {int l = 0, u = n−1;while (l <= u) {int m = (l + u) / 2;if (t[m] < v)l = m + 1;else if (t[m] > v)u = m − 1;else return m;}return −1;}To concentrate first on memory safety only, we declare two pragmas as above. The first pragma dictates that integers in C programs behave as infinite-precision mathematical integers, without overflows.The second pragma instructs the plug-in to ignore termination issues.Let’s call Frama-C with the Jessie plug-in on this program:> frama-c -jessie binary-search.cFigure 2.1 shows the result after10Safety CheckingFigure 2.1: Memory safety with no annotations• clicking on Alt-Ergo button to launch Alt-Ergo on both Safety and Normal behavior.

The normalbehavior is proved valid but not the safety.• selecting the raw “safety” and clicking on the button “split” to split the VC in parts. 3 sub-goalsare obtained: one that states the divisor 2 is not null, and two more that state the array access t[m]should be within bounds.• clicking again on Alt-Ergo, then CVC3 then Z3The remaing VC cannot be proved.Indeed, it is false that, in any context, functionbinary_search is memory safe. To ensure memory safety, binary_search must be called ina context where n is positive and array t is valid between indices 0 and n-1 included.