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

[Frama-c-discuss] Problem of "AXIOM"



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>