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>
- Follow-Ups:
- [Frama-c-discuss] Pragma declaration problem
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Pragma declaration problem
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Pragma declaration problem
- Next by Date: [Frama-c-discuss] Pragma declaration problem
- Next by thread: [Frama-c-discuss] Pragma declaration problem
- Index(es):