Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579
ID0002182: This issue was created automatically from Mantis Issue 2182. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002182 | Frama-C | Plug-in > wp | public | 2015-10-27 | 2015-10-27 |
| Reporter | lorenz | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
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 ^ : note: this is the location of the previous definition /tmp/ppannotc0c3e2.c:2:0: warning: "STDC_UTF_16" redefined #define STDC_UTF_16 1 ^ : note: this is the location of the previous definition /tmp/ppannotc0c3e2.c:3:0: warning: "STDC_UTF_32" redefined #define STDC_UTF_32 1 ^ : 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