Jessie Plugin, страница 3

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Chapter 5Reference Manual5.1General usageThe Jessie plug-in is activated by passing option -jessie to frama-c. Running the Jessie plug-in ona file f.jc produces the following files:• f.jessie: sub-directory where every generated files go• f.jessie/f.jc: translation of source file into intermediate Jessie language• f.jessie/f.cloc: trace file for source locationsThe plug-in will then automatically call the Jessie tool of the Why platform to analyze the generatedfile f.jc above. By default, VCs are generated using Why3 VC generator and displayed in the Why3IDEinterface.

Using -jessie-atp=gui option will use the Why2 VC generator and display in the WhyGUI interface, as it was the default in version 2.29 and before (deprecated).The -jessie-atp=<p> option allows to run VCs in batch, using the given theorem prover <p>.It uses the Why2 VC generator only, and is thus deprecated.

Running prover in batch mode after usingthe Why3 VC generator can be done using the Why3 tool why3 replay, see Why3 manual for details.5.2Unsupported features5.2.1Unsupported C featuresArbitrary gotosonly forward gotos, not jumping into nested blocks, are allowed. There is no plan to supportarbitrary gotos in a near future.Function pointersThere is no plan to support them in a near future.

In some cases, Frama-C’s specialization plug-incan be used to remove function pointers.Arbitrary cast• from integers to pointers, from pointer to integers: no support• between pointers: experimental support, only for casts in code, not logicNote: casts between integer types are supported22Reference ManualUnion typesexperimental support, both in code and annotationsVariadic C functionsunsupportedvolatile declaration modifiernot supportedconst declaration modifieraccepted but not taken into account, that is treated as non-const.5.2.2partially supported ACSL featuresInductive predicatessupported, but must follow the positive Horn clauses style presented in the ACSL documentation.Axiomatic declarationssupported (experimental)5.2.3Unsupported ACSL featuresLogic language• direct equality on structures is not supported.

Equality of each field should be used instead(e.g. by introducing an adequate predicate). Similarly, direct equality of arrays is not supported, and equality of each cells should be used instead.• array and structure field functional modifiers are not supported• higher-order constructs \lambda, \sum, \prod, etc. are not supportedLogic specifications• model variables and fields• global invariants and type invariants• volatile declarations• \initialized and \specified predicatesContract clauses• terminates clause• abrupt termination clauses• general code invariants (only loop invariants are supported)Ghost code• it is not checked whether ghost code does not interfere with program code.• ghost structure fields are not supportedC.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20175.3 Command-line options5.323Command-line options-jessie activates the plug-in, to perform C to Jessie translation-jessie-project-name=<s> specify project name for Jessie analysis-jessie-behavior=<s> restrict verification to the given behavior (safety, default or a user-definedbehavior)-jessie-std-stubs (obsolete) use annotated standard headers-jessie-hint-level=<i> level of hints, i.e. assertions to help the proof (e.g. for string usage)-jessie-infer-annot=<s> infer function annotations (inv, pre, spre, wpre)-jessie-abstract-domain=<s> use specified abstract domain (box, oct or poly)-jessie-jc-opt=<s> give an option to the jessie tool (e.g., -trust-ai)-jessie-why3=<command> alternative command used to call Why3 (default is “ide”)5.4PragmasInteger model# pragma JessieIntegerModel(value)Possible values: math, defensive, modulo.Default value: defensive• math: all int types are modeled by mathematical, unbounded integers ;• defensive: int types are modeled by integers with appropriate bounds, and for each arithmetic operations, it is mandatory to show that no overflow occur ;• modulo: models exactly machine integer arithmetics, allowing overflow, that is results mustbe taken modulo 2n for the appropriate n for each type.Floating point model# pragma JessieFloatModel(value)Possible values: math, defensive, full, multirounding.Default value: defensive.• math: all float types are modeled by mathematical unbounded real numbers• defensive: float types are modeled by real numbers with appropriate bounds and roundings, and for each floating-point arithmetic operations, it is mandatory to show that no overflow occur.

This model follows the IEEE-754 standard, under its strict form, as explainedin [2, 3].• full: models the full IEEE-754 standard, including infinite values and NaNs. This modelis the full model discussed in [2, 3].C. Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 201724Reference Manual• multirounding: models floating-point arithmetics so as to support combinations of compilerd and architectures that do not strictly follows IEEE-754 standard (e.g.

double roundings, 80-bits extended formats, compilation usinf fused-multiply-add instructions). This isbased on paper [5, 6].Floating point rounding mode# pragma JessieFloatRoundingMode(value)Possible values: nearesteven, down, up, tozero, nearestaway.Default value: nearesteven.Separation policy# pragma SeparationPolicy(value)Possible values: none, regionsInvariant policy# pragma InvariantPolicy(value)Possible values: none, arguments, ownershipTermination policy# pragma JessieTerminationPolicy(value)Possible values: always, never, userDefault: always• always means that every loop and every recursive function should be proved terminating.If they are not annotated by variants, then an unprovable VC (0 < 0) is generated.• user means that VCs for termination are generated for each case where a loop or functionvariant is given.

Otherwise no VC is generated.• never means no VC for termination are ever generated, even for annotated loop or recursivefunction.5.5TroubleshootingHere is a set of common error messages and possible fix or workaround.unsupported "cannot handle this lvalue" this message may appear in the following situations:• use an array as a parameter of a logic function.

You should use a pointer instead.unsupported "this kind of memory access is not currently supported" this message may appear inthe following situations:• equality on structures in the logic. The workaround is to check equality field by field. Tip:define field-by-field equality as a logic predicate.C.

Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 20175.5 Troubleshooting25unsupported "Jessie plugin does not support struct or union as parameter to logic functions."This is already quite explicit: jessie does not support structures or unions as a parameter of logicfunctions or predicates. You can circumvent this limitation by using an indirection via a pointer.unsupported "cannot take address of a function" The jessie plugin does not support functions as parameters to other functions. There is no simple workaround.

One thing you can try is to removethe function parameter and use a fixed abstract function (i.e. with a contract but no body), and thenprove that all the functions that might be passed as parameters respect this contract.unsupported "Type builtin_va_list not allowed" Jessie does not handle varyadic functions. The sametrick as above could be attempted.unsupported "Casting from type <..> to type <..> not allowed" Jessie does not support this cast, typically between pointer and integer. There is no simple workaround. One way of proving such kindof code is to replace the casts by an abstract function, whose post-condition explicitly explainshow the conversion is made.failure: cannot interpreted this lvalue This may happen if• using a structure in an assigns clause.

You need to expand ans say which field are assigned.C. Marché, Y. MoyWhy platform, Jessie plugin for Frama-CToccata, August 23, 201726C. Marché, Y. MoyReference ManualWhy platform, Jessie plugin for Frama-CToccata, August 23, 2017Bibliography[1] The Why verification tool. http://why.lri.fr/.[2] Ali Ayad and Claude Marché.

Behavioral properties of floating-point programs. Hisseo publications,2009. http://hisseo.saclay.inria.fr/ayad09.pdf.[3] Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesland Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, LectureNotes in Artificial Intelligence, Edinburgh, Scotland, July 2010. Springer.[4] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html.[5] Sylvie Boldo and Thi Minh Tuyen Nguyen.

Hardware-independent proofs of numerical programs.Hisseo publications, 2009. http://hisseo.saclay.inria.fr/tuyen09.pdf.[6] Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs.In César Mu noz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASAConference Publication, pages 14–23, Washington D.C., USA, April 2010.[7] Harvey Tuch, Gerwin Klein, and Michael Norrish.

Types, bytes, and separation logic. In Martin Hofmann and Matthias Felleisen, editors, Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principlesof Programming Languages (POPL’07), pages 97–108, Nice, France, January 2007..