2021-02-27 11:12 CET
  

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 
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 Files
  • c file icon test_wp_longlong.c (228 bytes) 2011-08-12 18:46 - 
    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;
}
    c file icon test_wp_longlong.c (228 bytes) 2011-08-12 18:46 +

-Relationships
+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.
+Notes

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