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



Hello B?rbara,

On 19/01/2012 19:14, B?rbara Vieira wrote:
> 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.

Well, jessie is behaving strangely here. In C, unsigned int array[10] as 
a formal argument is strictly equivalent to unsigned int* array (you can 
use unsigned int array[static 10] to mean that you pass an adress to the 
first element of an array of size at least 10, but this is not really 
supported by Frama-C plug-ins).

In the pointer case, you're missing an invariant on the value of array 
(Namely, loop1 says that it is incremented by 1 at each step, but there 
is no relation with the initial value.
Something like
loop invariant array ? \at(array,Pre)+(\at(len,Pre)-len);
should do the trick.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile