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
Assigned Toyakobowski 
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/", line 551, characters 30-32 Called from file "", line 134, characters 6-20 Called from file "src/kernel/", line 36, characters 4-20 Called from file "src/kernel/", line 723, characters 2-9 Called from file "src/kernel/", line 200, characters 4-8 Frama-C aborted because of internal error. Please report as 'crash' at 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
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker