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



Idem for the function assigns clause ;)

On 03/05/2011 13:43, 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/22b0f38b/attachment.htm>