--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP + assign clause



Hi everyone,

I'm working on some simple examples but I can't prove the following:

double v1[2];
double v2[2];

int index;

/*@	requires \valid_range(v1, 0, 1) && \valid_range(v2, 0, 1);
	assigns v1[0..1];
 	ensures \forall integer n; 0 <= n < 2 ==> 
 		v1[n] == v2[n];
*/
void fun(void){

	//Link invariant from output to Inv
	/*@	loop invariant 0 <= index <= 2;	
		loop assigns v1[0..index-1];
 		loop invariant \forall integer n; 0 <= n < index ==> 
			v1[n] == v2[n];
		loop variant 2-index;
	*/
	for(index=0; index <2; ++index){
		v1[index] = v2[index];
	}
}

Here is the result of the analysis:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: PastedGraphic-1.tiff
Type: image/tiff
Size: 83208 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110502/b25b706d/attachment-0001.tiff>
-------------- next part --------------


Does anyone knows why the assign clause is not good ?
Everything works fine without the assign clauses.

Arnaud