--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on November 2011 ---
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(); }