View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002420 | Frama-C | Plug-in > wp | public | 2018-12-28 00:58 | 2020-09-09 16:21 | ||||
Reporter | frederic.loulergue@nau.edu | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | resolved | Resolution | fixed | ||||||
Platform | Mac | OS | macOS | OS Version | Mojave 10.14.1 | ||||
Product Version | Frama-C 18-Argon | ||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002420: Wp crashes on a recursive function | ||||||||
Description | frama-c -wp tmp.c give the following trace. If the recursive call in e_get is removed, no crash. [kernel] Parsing tmp.c (with preprocessing) [wp] Running WP plugin... [kernel] Current source was: tmp.c:14 The full backtrace is: Raised by primitive operation at file "src/kernel_services/ast_data/statuses_by_call.ml", line 198, characters 11-65 Called from file "list.ml", line 82, characters 20-23 Called from file "src/kernel_services/ast_data/statuses_by_call.ml", line 231, characters 6-150 Called from file "src/plugins/wp/cil2cfg.ml", line 859, characters 6-35 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52 Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51 Called from file "src/plugins/wp/cil2cfg.ml", line 1216, characters 13-47 Called from file "src/plugins/wp/cil2cfg.ml", line 1248, characters 6-30 Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22 Called from file "src/plugins/wp/cil2cfg.ml" (inlined), line 1288, characters 13-33 Called from file "src/plugins/wp/wpAnnot.ml", line 1291, characters 12-26 Called from file "src/plugins/wp/wpAnnot.ml", line 1307, characters 12-28 Called from file "src/plugins/wp/wpAnnot.ml", line 1320, characters 16-68 Called from file "src/plugins/wp/Generator.ml", line 109, characters 4-67 Called from file "map.ml", line 291, characters 20-25 Called from file "src/plugins/wp/Generator.ml", line 137, characters 4-39 Called from file "src/plugins/wp/register.ml", line 686, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48 Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8 Unexpected error (Stack overflow). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is 18.0 (Argon). 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 |
|
![]() |
|
AllanBlanchard (developer) 2020-09-09 16:21 |
Fixed in the upcoming version of Frama-C. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2018-12-28 00:58 | frederic.loulergue@nau.edu | New Issue | |
2018-12-28 00:58 | frederic.loulergue@nau.edu | Status | new => assigned |
2018-12-28 00:58 | frederic.loulergue@nau.edu | Assigned To | => correnson |
2018-12-28 00:58 | frederic.loulergue@nau.edu | File Added: tmp.c | |
2019-10-17 15:35 | correnson | Status | assigned => acknowledged |
2020-09-09 16:21 | AllanBlanchard | Note Added: 0006979 | |
2020-09-09 16:21 | AllanBlanchard | Status | acknowledged => resolved |
2020-09-09 16:21 | AllanBlanchard | Resolution | open => fixed |