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