--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on January 2012 ---
Hello B?rbara, On 19/01/2012 12:33, B?rbara Vieira wrote: > @ case ind_case{L1,L2,L3}: > @ \forall unsigned int len1,len2,len3; > @ \forall unsigned int* result; > @ \forall unsigned int* array; > @ loop1{L1,L2}(len1,len2,result,array) ==> > @ len3 == len2 -1 ==> > @ \at(*result,L3) == (\at(*result,L2) & \at(array[0],L2)) ==> > @ //\at(array,L3) == \at(array,L2) + 1 ==>//Line that corresponds to array++ > @ loop1{L1,L3}(len1,len3,result,array); Jessie is right: your loop invariant is not correct. Namely, in your formula, array is a logical variable. Hence, its value does not depend on a given C memory state, and you have \at(array,L3) == \at(array,L2), for any L2,L3 (thus \at(array,L3) != \at(array,L2)+1). If you want to use this inductive to write your invariant, you have to use two distinct logical variables array1 and array2 in your inductive case: \forall unsigned int len1,len2,len3; \forall unsigned int* result; \forall unsigned int* array1,*array2; loop1{L1,L2}(len1,len2,result,array1) ==> len3 == len2 -1 ==> \at(*result,L3) == (\at(*result,L2) & \at(array1[0],L2)) ==> array2 == array1 + 1 ==> //Line that corresponds to array++ loop1{L1,L3}(len1,len3,result,array2); (BTW, I'm not sure you need two distincts len arguments in loop1, this could be handled similarly). -- E tutto per oggi, a la prossima volta Virgile