--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2011 ---
On Fri, Aug 12, 2011 at 12:54 PM, mars Gu <marsishandsome at gmail.com> wrote: > > In the file "problem_of_define.c", I define "true" as "1", by using the > following code: "#define true ((int)1)". > But Frama-c gives such error information: " unbound logic variable true in > annotation.". > It will be better, if wp can recognize "#define". > Wp sees the Abstract Syntax Tree, built from the pre-processed files. Pre-processing does not happen inside the comments (indeed, comments are removed by the pre-processor), as specified per 5.1.1.2 paragraph 3 in the C99 standard. See Q4 page 73 of http://frama-c.com/download/frama-c-value-analysis.pdf . This information is also available elsewhere since it is not specific to plug-in Value but this is where I remember to find it. In the file "problem_of_int_max.c", the const "INT_MAX" is used. > But Frama-c give the following error info: "unbound logic variable INT_MAX > in annotation.". > I think the problem is, that wp can process "#define" command. > Yes. The problem and solution are identical. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110812/1a54cb09/attachment.htm>