Crash when running "frama-c -jessie -jessie-atp=gui reduce.c"
ID0001790: This issue was created automatically from Mantis Issue 1790. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001790 | Frama-C | Plug-in > jessie | public | 2014-05-29 | 2016-06-21 |
| Reporter | johan | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | Linux | OS Version | Debian Jessie |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
Running "frama-c -jessie -jessie-atp=gui" on a simpler file works, but on the attached file, it produces an ml backtrace and asks me to report it as a crash to the BTS.
Additional Information :
The -enable-journal option, which the bug reporting guidelines encourage me to use, only tells me user "error: option `-enable-journal' is unknown."
Full output: $ frama-c -jessie -jessie-atp=gui reduce.c [kernel] preprocessing with "gcc -C -E -I. -dD reduce.c" [jessie] Starting Jessie translation [kernel] Current source was: reduce.c:15 The full backtrace is: Raised at file "norm.ml", line 769, characters 52-64 Called from file "norm.ml", line 772, characters 47-69 Called from file "list.ml", line 55, characters 20-23 Called from file "norm.ml", line 788, characters 43-62 Called from file "src/kernel/visitor.ml", line 162, characters 14-30 Called from file "src/kernel/visitor.ml", line 384, characters 21-46 Called from file "list.ml", line 66, characters 22-25 Called from file "src/kernel/visitor.ml", line 382, characters 8-398 Called from file "src/kernel/visitor.ml", line 583, characters 29-45 Called from file "src/kernel/visitor.ml", line 784, characters 6-21 Called from file "cil/src/cil.ml", line 3280, characters 5-53 Called from file "cil/src/cil.ml", line 5881, characters 17-37 Called from file "cil/src/cil.ml", line 5888, characters 3-20 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 5905, characters 15-39 Called from file "norm.ml", line 1875, characters 2-27 Called from file "register.ml", line 159, characters 4-23 Called from file "register.ml", line 327, characters 6-12 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Unexpected error (File "norm.ml", line 769, characters 52-58: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelinesSteps To Reproduce :
Run "frama-c -jessie -jessie-atp=gui reduce.c" with the attached file reduce.c