--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with "#define" and "INT_MAX"



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>