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] \Old struct value

Hi everyone,

I'm trying to prove some code and I'm stuck with the following proof.
The problem is in the "compute" method. I have a structure containing 
some input and output data and an other structure containing a memory. 
The compute method does the following simple thing:
	- The output is set to the value of the memory
	- The memory is updated with the input value.

I would like to proof with WP and cvc3 that at the end of the compute 
method, these values are correct.
So my probleme here is about the usage of the \Old(...) and \at(...,Pre) 
constructs (the only things I can't proof are:
	- get_mem_invariant.
	- compute method post condition.

Can anyone help me to figure out what is happening ?

Thanks.
Arnaud

myFile.c:

typedef struct{
	double d_in[2];
	double d_out[2];
}t_struct;

typedef struct{
	double d_mem[2];
}t_struct_memory;

t_struct b;
t_struct_memory mem;

/*@ 	requires \valid(&mem.d_mem);
  	ensures \forall integer n; 0 <= n < 2 ==> mem.d_mem[n] == 0.0;
*/
void init(){
	int i=0;
	/*@
   		loop invariant init_mem_invariant: \forall integer n; 0 <= n < i 
==> mem.d_mem[n] == 0.0;
   		loop variant 2-i;
  	*/
	for (i=0;i<2;++i){
		mem.d_mem[i] = 0.0;
	}
}

/*@	requires \forall integer n; 0 <= n < 2 ==>
		\valid(&b.d_in+n) && \valid(&b.d_out+n) && \valid(&mem.d_mem+n);
	ensures \forall integer n; 0 <= n < 2 ==>
		b.d_out[n] == \old(mem.d_mem[n]) &&
		mem.d_mem[n] == b.d_in[n];
  */
void compute(){

	int i=0;
	/*@	
		loop invariant get_mem_invariant: \forall integer n; 0 <= n < i ==>
			b.d_out[n] == \at(mem.d_mem[i],Pre);
		loop invariant set_mem_invariant: \forall integer n; 0 <= n < i ==>
			mem.d_mem[n] == b.d_in[n];
		loop variant 2-i;
	*/
	for (i=0;i<2;++i){
		b.d_out[i] = mem.d_mem[i];
		mem.d_mem[i] = b.d_in[i];
	}
}

void main(int argc,char** argv[]){

	init();
	compute();

}