--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Local variables leading to



Dear all,

currently I try to verify a C program with local variables that are passed to 
subroutines using the address operator. I could reduce the problem to the 
following, almost minimal, version:

--------------------------
typedef struct _my_type {int i; int j;} my_type;

/*@
  assigns (*s);
  ensures s->i == \old(s->j);
*/
void my_changes (my_type* s){s->i = s->j;};

/*@
  assigns \result;
  ensures \result == \old(n);
*/
int my_main (int n){
  my_type t;
  t.j=n;
  my_changes(&t);
  return t.i;
}
--------------------------
Unfortunately,  trying to translate this to the COQ backend with
	frama-c -jessie -jessie-atp coq local_var.c
I get the following error:
	...
	[jessie] Calling VCs generator.
	why -coq [...] why/local_var.why
	File "why/local_var.why", line 447, characters 24-49:
	Unbound variable _my_type_t_2_alloc_table
	...

When I tried the translation without the "assigns", the translation is 
possible but the verification conditions of my (longer) progamm were not 
provable, as they assumed that not assignments were done...

If the variable t in my_main is not local but global instead, then translation 
is again possible, but this is quite far from what I want to prove...

So what can I do? Is there perhaps a bug in jessie when processing local 
variables? (I currently use frama-c-Boron-20100401-why-2.24.tar.gz)


Regards, Norbert
-- 
Priv.-Doz. Dr. Norbert Mueller
FB IV * Informatik * Universitaet Trier * D-54286 Trier (Germany)
email: mueller at uni-trier.de    * http://www.uni-trier.de/~mueller/
Tel: ..49-(0)651-201-2845/3875 * Fax: ..49-(0)651-201-3805