2021-02-27 10:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001116Frama-CKernelpublic2014-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)

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)

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

~0004705

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