Frama-C Bug Tracking System - Frama-C
View Issue Details
0001005Frama-CKernelpublic2011-10-28 17:152012-09-19 17:16
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001005: defining two axioms with same name causes kernel crash
DescriptionRunning "frama-c -cpp-command 'gcc -C -E -I.' -jessie '-jessie-why-opt=-exp goal' -no-unicode -jessie-atp simplify list.c" under why 2.30 on the attached program caused a kernel crash, asking to report it here. The last output was:

[kernel] failure: trying to register twice property `axiom
                  That is forbidden (kernel invariant broken).
[kernel] The full backtrace is:
         Raised at file "src/kernel/", line 509, characters 30-31
         Called from file "src/kernel/", line 503, characters 9-16
         Re-raised at file "src/kernel/", line 506, characters 15-16
         Called from file "src/logic/", line 349, characters 4-132
         Called from file "", line 69, characters 12-15
         Called from file "", line 69, characters 12-15
         Called from file "src/kernel/", line 1196, characters 5-43
         Called from file "src/kernel/", line 1412, characters 4-27
         Called from file "src/kernel/", line 64, characters 2-28
         Called from file "src/project/", line 490, characters 17-21
         Called from file "src/kernel/", line 33, characters 60-72
         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

The program "list.c" is obviously faulty, as it defines two axioms with the same name "inj1".
TagsNo tags attached.
Attached Filesc list.c (69) 2011-10-28 17:15

There are no notes attached to this issue.

Issue History
2011-10-28 17:15JochenNew Issue
2011-10-28 17:15JochenFile Added: list.c
2011-10-30 22:40svn
2011-10-30 22:40svnStatusnew => resolved
2011-10-30 22:40svnResolutionopen => fixed
2011-10-31 19:28signolesStatusresolved => assigned
2011-10-31 19:28signolesAssigned To => virgile
2011-10-31 19:28signolesStatusassigned => resolved
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed