Skip to content

defining two axioms with same name causes kernel crash

ID0001005: This issue was created automatically from Mantis Issue 1005. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001005 Frama-C Kernel public 2011-10-28 2012-09-19
Reporter Jochen Assigned To virgile Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version Frama-C Oxygen-20120901

Description :

Running "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 inj1'. That is forbidden (kernel invariant broken). [kernel] The full backtrace is: Raised at file "src/kernel/log.ml", line 509, characters 30-31 Called from file "src/kernel/log.ml", line 503, characters 9-16 Re-raised at file "src/kernel/log.ml", line 506, characters 15-16 Called from file "src/logic/property_status.ml", line 349, characters 4-132 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "src/kernel/file.ml", line 1196, characters 5-43 Called from file "src/kernel/file.ml", line 1412, characters 4-27 Called from file "src/kernel/ast.ml", line 64, characters 2-28 Called from file "src/project/state_builder.ml", line 490, characters 17-21 Called from file "src/kernel/boot.ml", line 33, characters 60-72 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/.

The program "list.c" is obviously faulty, as it defines two axioms with the same name "inj1".

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information