Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000925Frama-CPlug-in > wppublic2011-08-12 18:462011-10-10 14:14
Reporterjessie_user 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000925: Wp rises an error in if you use struct and long long type, with wp-rte option
DescriptionFollowing 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 Informationstruct 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; }
TagsNo tags attached.
Attached Filesc file icon test_wp_longlong.c [^] (228 bytes) 2011-08-12 18:46 [Show Content]

- Relationships

-  Notes
(0002144)
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).
(0002146)
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.
(0002270)
monate (reporter)
2011-09-14 19:38

 Fixed in current version of trunk.

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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker