# Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [Frama-c-discuss] Pragma declaration problem

*Subject*: [Frama-c-discuss] Pragma declaration problem*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Tue, 06 Apr 2010 16:13:43 +0200*In-reply-to*: <l2kb489c431004030536t9883d645q4ed52149ce7ebdec@mail.gmail.com>*References*: <l2kb489c431004030536t9883d645q4ed52149ce7ebdec@mail.gmail.com>

An Nguyen wrote: > Dear list member, > > When I read jessie-tutorial.pdf and tried something on it, I found a pragma > declaration described on page 26 of this document wasn't as same as in real > Jessie plugin. > The syntax of pragma on floating point model is described as follow: #pragma > FloatModel(value). But actually, its syntax is #pragma > JessieFloatModel(value). > You're right, it is a mistake in the manual, and you guessed well, the pragma is "JessieFloatModel". > Moreover, some arguments seemed to work incorrectly in my system. I don't > know the reason. > > With this example: > > #pragma JessieFloatModel( < arg> ) > /*@ > requires radius>0; > ensures \abs(\result - 3.141592654*2.0*radius) <= 0.01; > */ > float Perimeter(float radius) { > return 2.0*3.14*radius; > } > > One by one, I replaced <arg> above by followings : "math", "real", "strict" > and "full" . Then, I had the result: > - math : it said that this value wasn't supported. > Right also. "math" was supposed to be an alias for "real" but does not work in the distributed version. Anyway, let me warn that in the future release, "math" will work and "real" will not ("real" is considered too ambiguous) > - real : all conditions were "unknown" in verification. > Pascal already answered that: without any bound on radius, your post-condition is wrong. But if you add radius <= 3 as pre-condition, the post-condition is proved both by Alt-Ergo, Z3 and CVC3. If you do not have these provers, you should install them, see http://why.lri.fr/provers.en.html > - strict: it couldn't solve the problem on overflow. > Here you want to consider the true computations that occur, taking rounding into account. Be aware that you enter a difficult area! To solve the VCs, you will need a prover that is dedicated to FP rounding, namely gappa (see the same page as above). With Gappa, I'm able to prove all VCs for your example. > - full: it caused time-out. > Indeed, I have the same behavior. Using the full model might generate VCs with complex propositional structure, which are hard for theorem provers. See Ayad & Marche's paper on http://hisseo.saclay.inria.fr/documents.html In short: do not use the "full" model unless you really need it (and in that case tell me more...) > I want to write specification for a single-procedure which has > floating-point numbers and PI number, and the rounding-error can be accepted > in a small range. I mean, if I write the ACSL-like annotation with PI number > as 3.141592654 and in C code with PI number as 3.14, the C source code will > valid in my verification. Would you please help me doing that ? > > As said before, add "radius <= 3.0" as precondition, and install more provers. > Another problem is to use #pragma JessieTerminationPolicy(value), when I > executed my verification, a warning showed that this pragma was ignored. How > can I use this pragma ? > Indeed, it is another mistake in the doc, since this pragma is not yet available in Jessie/Why 2.23. With this version, you have to ignore the unproved VC, or add a proper variant. Sorry about that. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |

**References**:**[Frama-c-discuss] Pragma declaration problem***From:*annguyen2210 at gmail.com (An Nguyen)

- Prev by Date:
**[Frama-c-discuss] ACSL by Example 4.2.1 released** - Next by Date:
**[Frama-c-discuss] Modélisation et vérification d'algorithmes en Coq** - Previous by thread:
**[Frama-c-discuss] Pragma declaration problem** - Next by thread:
**[Frama-c-discuss] ACSL by Example 4.2.1 released** - Index(es):