0000925: Wp rises an error in if you use struct and long long type, with wp-rte option

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

test_wp_longlong.c [^] (228 bytes) 2011-08-12 18:46 [Show Content] [Hide Content]

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;
}

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