Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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