Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Jessie: Local variables leading to
  • From: mueller at uni-trier.de (Norbert Müller)
  • Date: Sun, 17 Oct 2010 17:00:49 +0200
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