2021-02-27 11:32 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001243Frama-CKernelpublic2012-09-19 17:16
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001243: two axioms with same name cause crash
DescriptionRunning "frama-c -wp ftest.c" on the attached program caused a crash, with the following output:
[kernel] preprocessing with "gcc -C -E -I. ftest.c"
[kernel] failure: trying to register twice property `axiom a1'.
                  That is forbidden (kernel invariant broken).
[kernel] The full backtrace is:
         Raised at file "src/wp/register.ml", line 551, characters 30-32
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 36, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
         Frama-C aborted because of internal error.
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Nitrogen-20111001.

TagsNo tags attached.
Attached Files
  • c file icon ftest.c (68 bytes) 2012-07-16 18:59 -
    /*@ axiomatic ax {
        axiom a1: 0==0;
        axiom a1: 1==1;
        }
    */
    
    c file icon ftest.c (68 bytes) 2012-07-16 18:59 +

-Relationships
+Relationships

-Notes

~0003301

yakobowski (manager)

Thanks for the report. This is actually already fixed in the trunk.

[kernel] preprocessing with "gcc -C -E -I. ftest.c"
ftest.c:3:[kernel] user error: a1 is already registered as axiom (ftest.c:2) in annotation.
+Notes

-Issue History
Date Modified Username Field Change
2012-07-16 18:59 Jochen New Issue
2012-07-16 18:59 Jochen File Added: ftest.c
2012-07-16 20:53 yakobowski Note Added: 0003301
2012-07-16 20:53 yakobowski Status new => resolved
2012-07-16 20:53 yakobowski Resolution open => fixed
2012-07-19 01:37 signoles Assigned To => yakobowski
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History