--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/Jessie: memory set problem



Hello,

Launching:
	frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c

with foo.c containing:

//*****************************************
typedef struct {int i;int j;} las;

/*@ requires \valid(a) && \valid(b);
    assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }

/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{  g (&(p->i), &(p->j)); }
//*****************************************

returns the following error:

memory (mem-field(int_M),b_21)
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 716, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 
7-13: Assertion failed
Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v 
  -locs foo.cloc foo.jc


Jessie/Why version is 2.18.

C code seems to be OK as Frama-C Value Analysis plug-in correctly 
analyzes it!
May this be a problem with Jessie?

Thanks in advance for your help!
Dillon PARIENTE