--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2011 ---
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>