--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on January 2012 ---
Hi Vergile, Thank you very much for the tip. It works now. Regarding this code, do you know why I can't prove its safety? The proof obligation related with dereferencing the pointer "array" at - *result &= array[0]; - is not provable. However, if instead of using a pointer to an unsigned int, it is used an array, such as: void increment_ptr_1(unsigned int array[10],unsigned int* result) { *result = 0xffaabbcc; unsigned int len = 10; while(len > 0) { *result &= array[0]; array++; len--; } } the proof obligation is not generated and all of the safety conditions are automatically proved. Can you explain me how the Jessie/Frama-C works here? I thought that using as a precondition \valid(array..(0..len-1)) (in the previous code) would be stronger than defining the argument as an array. Best regards, B?rbara On 19/01/2012, at 12:28, Virgile Prevosto wrote: > 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 > > _______________________________________________ > 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