View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000925 | Frama-C | Plug-in > wp | public | 2011-08-12 18:46 | 2011-10-10 14:14 | ||||
Reporter | jessie_user | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20101202-beta2 | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000925: Wp rises an error in if you use struct and long long type, with wp-rte option | ||||||||
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; } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
pascal (reporter) 2011-08-12 22:21 |
Thanks for the report. If you are using a version of Frama-C compiled with a 32-bit OCaml compiler, you can make the error less likely by using a 64-bit OCaml compiler to recompile it. Once the bug is fixed, then you can again use any sort of OCaml compiler (32 or 64-bit). |
jessie_user (reporter) 2011-08-15 17:39 |
Thank you for your quick answer. I have tried ocaml64-bit compiler and it has succeeded. Unfortunately I've got another wp-plugin error with new installation. |
monate (reporter) 2011-09-14 19:38 |
Fixed in current version of trunk. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-08-12 18:46 | jessie_user | New Issue | |
2011-08-12 18:46 | jessie_user | Status | new => assigned |
2011-08-12 18:46 | jessie_user | Assigned To | => correnson |
2011-08-12 18:46 | jessie_user | File Added: test_wp_longlong.c | |
2011-08-12 22:21 | pascal | Note Added: 0002144 | |
2011-08-15 17:39 | jessie_user | Note Added: 0002146 | |
2011-09-14 19:38 | monate | Note Added: 0002270 | |
2011-09-14 19:38 | monate | Status | assigned => resolved |
2011-09-14 19:38 | monate | Fixed in Version | => Frama-C GIT, precise the release id |
2011-09-14 19:38 | monate | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |