--- layout: fc_discuss_archives title: Message 4 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,
  Your loop assign claus is incomplete, index is also modify in the loop 
body:

  loop assign v1[0..index-1], index ;

Best

On 02/05/2011 18:24, Arnaud Dieumegard wrote:
> 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:
>
>
>
>
>
> Does anyone knows why the assign clause is not good ?
> Everything works fine without the assign clauses.
>
> Arnaud
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110503/22085285/attachment.htm>