2021-02-27 10:26 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001116Frama-CKernelpublic2012-03-12 10:262014-02-12 16:59
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytrivialReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001116: axiom outside axiomatic tacitly ignored in presence of struct
DescriptionRunning frama-c -wp on the attached program doesn't produce a syntax error message, although using "axiom" outside "axiomatic" is incorrect.

However, the axiom is not given to the provers: alt-ergo can't verify the program, but it will verify it if "axiom" is changed to "lemma" (in that case, the lemma is given to alt-ergo).

If the struct in line 6-8 is removed, a syntax error is reported as expected (however at EOF position, which seems too late).
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (135 bytes) 2012-03-12 10:26 - 
    /*@ axiom l:
    \forall int i; i < 0;
 */

struct _str {
    int x;
};

//@ ensures \result < 0;
int ftest(int i) {
    return i;
}
    c file icon ftest.c (135 bytes) 2012-03-12 10:26 +

-Relationships
+Relationships

-Notes

~0002757

Jochen (reporter)

2012-03-12 10:30

 Concerning the late syntax error position at EOF, there may be a connection to issue 0000840 "syntax error message refers to (true error line + 5 lines)".

~0002758

signoles (manager)

2012-03-12 10:47

 Agree: an axiom outside an axiomatic should produce an error from the kernel.

~0004705

2014-02-12 16:59

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-03-12 10:26 Jochen New Issue
2012-03-12 10:26 Jochen Status new => assigned
2012-03-12 10:26 Jochen Assigned To => correnson
2012-03-12 10:26 Jochen File Added: ftest.c
2012-03-12 10:30 Jochen Note Added: 0002757
2012-03-12 10:46 signoles Assigned To correnson => virgile
2012-03-12 10:47 signoles Note Added: 0002758
2012-03-12 10:47 signoles Category Plug-in > wp => Kernel
2012-04-02 15:51 svn
2012-04-02 15:51 svn Status assigned => resolved
2012-04-02 15:51 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master 6134fa2e
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 6134fa2e
2014-02-12 16:59 Note Added: 0004705
2014-02-12 16:59 Status closed => resolved
+Issue History