--- layout: fc_discuss_archives title: Message 7 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"



Hi,

I have some problems by using the preprocessing command "define" and the
predefined const "INT_MAX".
My Frama-C version is "Frama-C Carbon-20110201+dev".
I start Frama-C with the following command:  "frama-c-gui -wp
-wp-proof alt-ergo program.c &".

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".

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.

Liangliang Gu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110812/f85faae1/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: problem_of_define.c
Type: text/x-csrc
Size: 123 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110812/f85faae1/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: problem_of_int_max.c
Type: text/x-csrc
Size: 126 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110812/f85faae1/attachment-0001.c>