--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2010 ---
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>