View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001790 | Frama-C | Plug-in > jessie | public | 2014-05-29 07:12 | 2016-06-21 14:08 | ||||
Reporter | johan | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | Linux | OS Version | Debian Jessie | |||||
Product Version | Frama-C Neon-20140301 | ||||||||
Target Version | Fixed in Version | Frama-C Aluminium | |||||||
Summary | 0001790: Crash when running "frama-c -jessie -jessie-atp=gui reduce.c" | ||||||||
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. | ||||||||
Steps To Reproduce | Run "frama-c -jessie -jessie-atp=gui reduce.c" with the attached file reduce.c | ||||||||
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_guidelines | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2014-05-29 11:17 |
Hi, Thanks for noticing the problem with -journal-enable/-enable-journal in the guidelines. This is now fixed. Although Jessie should not have crashed, the problem you encounter is actually in your specification. You should write 'assigns tab[0 .. n-1]' (or equivalently 'assigns *(tab+(0 .. n-1))', not 'assigns tab+(0 .. n-1)' |
johan (reporter) 2014-05-29 17:45 |
Thanks for the quick reply, which solves the problem I had. I expected that my specification was incorrect, as I am a beginner and I do not expect a crash for a correct test-case that is as simple as mine. Thanks again. |
yakobowski (manager) 2016-02-09 16:21 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-05-29 07:12 | johan | New Issue | |
2014-05-29 07:12 | johan | Status | new => assigned |
2014-05-29 07:12 | johan | Assigned To | => cmarche |
2014-05-29 07:12 | johan | File Added: reduce.c | |
2014-05-29 11:17 | yakobowski | Note Added: 0005170 | |
2014-05-29 17:45 | johan | Note Added: 0005174 | |
2015-10-23 15:26 | yakobowski | Assigned To | cmarche => yakobowski |
2016-02-09 16:21 | yakobowski | Source_changeset_attached | => framac master 9e13dd98 |
2016-02-09 16:21 | yakobowski | Note Added: 0006154 | |
2016-02-09 16:21 | yakobowski | Status | assigned => resolved |
2016-02-09 16:21 | yakobowski | Resolution | open => fixed |
2016-06-21 14:08 | signoles | Fixed in Version | => Frama-C Aluminium |
2016-06-21 14:08 | signoles | Status | resolved => closed |