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



> I’ve been trying to get a working bubble sort implementation to verify using the latest frama-c and WP plugin. After failing for a few days, I tried narrowing my problems down to simpler tasks. The following code is supposed to(!) bubble up the maximum value of the array to the position a[end-1] of the array, but notice that I intentionally modified the code so that it doesn’t change the array at all. Nevertheless, the WP plugin reports valid for all the proof goals, including the post-condition. Am I missing something obvious here?

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).

	L.