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



> 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