2021-01-21 05:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002182Frama-CPlug-in > wppublic2015-10-27 23:25
Assigned Tocorrenson 
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002182: Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579
DescriptionThe 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:
Steps To Reproduceframa-c -wp min3.c
TagsNo tags attached.
Attached Files
  • c file icon min3.c (491 bytes) 2015-10-27 21:08 -
    #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); */
    c file icon min3.c (491 bytes) 2015-10-27 21:08 +

duplicate of 0002158closedvirgile WP crashes on the given function 

There are no notes attached to this issue.

-Issue History
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
+Issue History