Jessie Tutorial (811290), страница 4

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 4)

The -jessie-atp=<p> optionallows to run VCs in batch, using the given theorem prover <p>.7.2Unsupported features7.2.1Unsupported C featuresArbitrary gotosonly forward gotos, not jumping into nested blocks, are allowed. There is no plan to support arbitrary gotosin a near future.Function pointersThere is no plan to support them in a near future. One should consider using the specialization plugin toremove 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 supportedUnion 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.247.2.2partially supported ACSL featuresInductive predicatessupported, but must follow the positive Horn clauses style presented in the ACSL documentation.Axiomatic declarationssupported (experimental)7.2.3Unsupported ACSL featuresLogic language• direct equality on structures is not supported.

Equality of each field should be used instead (e.g. byintroducing an adequate predicate). Similarly, direct equality of arrays is not supported, and equalityof 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 fieldsglobal invariants and type invariantsvolatile 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 supported7.3Command-line options-jessie activates the plugin, to perform C to Jessie translation-jessie-project-name=<s> specify project name for Jessie analysis-jessie-atp=<s> do not launch the GUI but run specified automated theorem prover in batch (among alt-ergo,cvc3, simplify, yices, z3), or just generate the verification conditions (goals)-jessie-cpu-limit=<i> set the time limit in sec.

for proving each VC. Only works when -jessie-atp is set.-jessie-behavior=<s> restrict verification to the given behavior (safety, default or a user-defined behavior)-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-why-opt=<s> give an option to Why (e.g., -fast-wp)257.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 arithmeticoperations, it is mandatory to show that no overflow occur ;• modulo: models exactly machine integer arithmetics, allowing overflow, that is results must be takenmodulo 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 foreach floating-point arithmetic operations, it is mandatory to show that no overflow occur.

This modelfollows the IEEE-754 standard, under its strict form, as explained in [1, 2].• full: models the full IEEE-754 standard, including infinite values and NaNs. This model is the fullmodel discussed in [1, 2].• multirounding: models floating-point arithmetics so as to support combinations of compilerd andarchitectures that do not strictly follows IEEE-754 standard (e.g. double roundings, 80-bits extendedformats, compilation usinf fused-multiply-add instructions). This is based on paper [3, 4].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: always26• always means that every loop and every recursive function should be proved terminating.

If they arenot 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 function variant isgiven. Otherwise no VC is generated.• never means no VC for termination are ever generated, even for annotated loop or recursive function.27Bibliography[1] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs.

Hisseo publications, 2009.http://hisseo.saclay.inria.fr/ayad09.pdf.[2] Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and ReinerHähnle, editors, Fifth International Joint Conference on Automated Reasoning, Lecture Notes in ArtificialIntelligence, Edinburgh, Scotland, July 2010. Springer.[3] Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. Hisseopublications, 2009. http://hisseo.saclay.inria.fr/tuyen09.pdf.[4] Sylvie Boldo and Thi Minh Tuyen Nguyen.

Hardware-independent proofs of numerical programs. In César Munoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication,pages 14–23, Washington D.C., USA, April 2010.[5] Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud,January 2009.[6] Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal ofSymbolic Computation, 2010. to appear.[7] Harvey Tuch, Gerwin Klein, and Michael Norrish. Types, bytes, and separation logic.

In Martin Hofmann andMatthias Felleisen, editors, Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages (POPL’07), pages 97–108, Nice, France, January 2007.28.

Характеристики

Список файлов книги