View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002182 | Frama-C | Plug-in > wp | public | 2015-10-27 21:08 | 2015-10-27 23:25 | ||||||||
Reporter | lorenz | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | Frama-C Sodium | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002182: Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579 | ||||||||||||
Description | The following (minimized) example file crashes the wp plugin of frama-c: #> frama-c -wp min3.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing min3.c (with preprocessing) /tmp/ppannotc0c3e2.c:1:0: warning: "__STDC_VERSION__" redefined #define __STDC_VERSION__ 201112L ^ <built-in>: note: this is the location of the previous definition /tmp/ppannotc0c3e2.c:2:0: warning: "__STDC_UTF_16__" redefined #define __STDC_UTF_16__ 1 ^ <built-in>: note: this is the location of the previous definition /tmp/ppannotc0c3e2.c:3:0: warning: "__STDC_UTF_32__" redefined #define __STDC_UTF_32__ 1 ^ <built-in>: note: this is the location of the previous definition [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] failure: *** Label Label 'L' not-found [kernel] Current source was: min3.c:16 The full backtrace is: Raised at file "src/wp/register.ml", line 579, characters 30-32 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 763, characters 2-9 Called from file "src/kernel/cmdline.ml", line 216, characters 4-8 Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Sodium-20150201. 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 #> | ||||||||||||
Steps To Reproduce | frama-c -wp min3.c | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-10-27 21:08 | lorenz | New Issue | |
2015-10-27 21:08 | lorenz | Status | new => assigned |
2015-10-27 21:08 | lorenz | Assigned To | => correnson |
2015-10-27 21:08 | lorenz | File Added: min3.c | |
2015-10-27 23:25 | yakobowski | Relationship added | duplicate of 0002158 |