--- layout: fc_discuss_archives title: Message 6 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,

Thanks for the answer.
It's all good now.

Best regards
Arnaud

On May 3, 2011, at 1:43 PM, Zaynah Dargaye wrote:

> 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
> 
> _______________________________________________
> 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/adcfd02d/attachment.htm>