Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001243Frama-CKernelpublic2012-07-16 18:592012-09-19 17:16
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon ftest.c [^] (68 bytes) 2012-07-16 18:59 [Show Content]

- Relationships

-  Notes
(0003301)
yakobowski (manager)
2012-07-16 20:53

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.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker