--- layout: fc_discuss_archives title: Message 39 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



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