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

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                    |