Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Problem of "AXIOM"
  • From: marsishandsome at gmail.com (mars Gu)
  • Date: Thu, 11 Aug 2011 15:13:37 +0200
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>