ID0000925: **This issue was created automatically from Mantis Issue 925. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000925 | Frama-C | Plug-in > wp | public | 2011-08-12 | 2011-10-10 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jessie_user | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 | ### Description : Following command with -wp-rte option rises an error. frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c Output: frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c [kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c" [rte] annotating function add [kernel] The full backtrace is: Raised at file "src/kernel/command.ml", line 42, characters 10-13 Called from file "src/wp/cfgProof.ml", line 125, characters 4-118 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "src/wp/cfgProof.ml", line 223, characters 1-607 Called from file "src/wp/register.ml", line 322, characters 41-57 Called from file "src/wp/register.ml", line 464, characters 3-32 Called from file "src/wp/register.ml", line 533, characters 8-20 Called from file "src/wp/register.ml", line 570, characters 4-18 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 660, characters 2-9 Called from file "src/kernel/cmdline.ml", line 173, characters 4-8 Unexpected error (Failure("int_of_string")). Please report as 'crash' at http://bts.frama-c.com/ Note that a backtrace alone often does not have 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 Without wp-rte Option ok: frama-c -wp -wp-out wp_longlong test_wp_longlong.c [kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c" [wp] warning: Missing RTE guards If you use int type in INTEGER32 structure, then its ok. ### Additional Information : struct INTEGER32 { // int value; // Ok long long value; // Fails }; typedef struct INTEGER32 int32; /*@ requires \valid(x) && \valid(y); */ void add (int32* x, int32* y){ int32 erg; erg.value = x->value + y->value; } ## Attachments - [test_wp_longlong.c](/uploads/821c2c96e2982d73b22a7f481b578648/test_wp_longlong.c)