--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on January 2012 ---
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