--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2011 ---
Hi, I meet some problems, when I try to define "AXIOM"s in the functions. In the file "count2.c", an AXIOM called "Count" is defined (with out labels). 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 count2.c &". Frama-C gives some Warnings. One example is like: "count2.c:63:[wp] warning: Warning for Axiom Count2: From wp: load of arbitrary region not yet implemented Effect: Ignored user-defined axiom 'Count2'". I don't understand what the warning information means. Would you please give me some explanation of this problem? Liangliang Gu -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110811/ddba5070/attachment-0001.htm> -------------- next part -------------- A non-text attachment was scrubbed... Name: count2.c Type: text/x-csrc Size: 1533 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110811/ddba5070/attachment-0001.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: count2.png Type: image/png Size: 36626 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110811/ddba5070/attachment-0001.png>