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,

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