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

It perfectly works now. I completely forgot to add such invariant.
Thank you very much for your help.

B?rbara


On 20/01/2012, at 17:49, Virgile Prevosto wrote:

> 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
> 
> _______________________________________________
> 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