--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin report incorrect



Your function *is* doing something, and the post-condition is exactly your loop invariant with (i == end), hence it finally holds.
	L.


> Le 5 oct. 2015 à 17:19, Christoph Rauch <christoph.rauch at fau.de> a écrit :
> 
> 
>> On 05 Oct 2015, at 16:54, Loïc Correnson <loic.correnson at cea.fr> wrote:
>> 
>> Yes ! Indeed, there is nothing about the preservation of the elements in the array across the function.
>> Something like :
>> /*@ …
>> ensures
>>    \forall integer i ; start <= i < end ==> 
>>    \exists integer j ; start <= j < end ==> a[i] == \old( a[j] ) ;
>> */
>> (and the other way).
> 
> Of course, that is a post-condition that should *also* hold in the final algorithm, and indeed I have formulated this using the Permut predicate from the Jessie tutorial. I only left it out here, because it didn’t change the result and it shouldn’t be a necessary condition. After all, the contract I gave would be fulfilled by a function that sets a[end-1] to INT_MAX. But doing nothing is not such a function and WP shouldn’t be able to prove that the post-condition holds.
> 
> --
> Christoph
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss