| 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 | |
| Platform | | OS | | OS Version | |
| 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
^
: 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 |
| Tags | No tags attached. |
|
| Attached Files |  min3.c [^] (491 bytes) 2015-10-27 21:08 [Show Content] [Hide Content]#define NULL 0
typedef struct linked_list_tree_struct tree_t;
struct linked_list_tree_struct {
tree_t* next_sibling;
};
/*@ inductive are_siblings{L} (tree_t *a, tree_t *b) {
}
*/
/*@ inductive reachable{L} (tree_t *root, tree_t *node) {
}
*/
/*@ predicate well_formed(tree_t *root) =
(root->next_sibling == NULL || well_formed(root->next_sibling));
*/
int main(int argc, char *argv[argc]) {
tree_t grandchild1 = { };
/*@ assert well_formed(&grandchild1); */
}
|
|
Relationships 
Notes