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: annguyen2210 at gmail.com (An Nguyen)
  • Date: Sat, 3 Apr 2010 19:36:47 +0700
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).
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.
- real : all conditions were "unknown" in verification.
- strict: it couldn't solve the problem on overflow.
- full: it caused time-out.

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 ?

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 ?

Thank you. I'm looking forward to your reply.

Best regards.


-- 
An Nhu Nguyen
Faculty of Computer Science and Engineering
Class: Honor Program 06
HCM City University of Technology
Mobile: 0909048788
Y!M: annguyencs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100403/90a94144/attachment.htm>