--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plug-in - Pointer arithmetic



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