--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2009 ---
Hello, Le lun 16 f?v 2009 14:19:12 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > copy_array (a + middle, length-middle, b); > //@ assert \forall integer i; 0 <= i < length-middle ==> a[i+middle] == b[i] ; > copy_array (a, middle, b + length-middle); > //@ assert \forall integer i; 0 <= i < middle ==> a[i] == b[i+length-middle] ; > //these lines get proven > > //regardless the first assertion, if it is placed again, after function call, the prover fails: > > //@ assert \forall integer i; 0 <= i < length-middle ==> a[i+middle] == b[i] ; The issue lies in the fact that you have commented out the assigns clause of copy_array. Without this clause, when analyzing rotate_array, there is no way to know that only the first part of b has changed (remember: the verification process is modular. when analyzing rotate_array, the only thing that is known of copy_array is its specification). With that clause, both Simplify and Z3 can prove the assertion. However, I have to admit that the assigns clause itself is not proved by any of the prover at this stage, and I don't currently have any suggestion as how to proceed. Anyway, I hope that this answer helps a bit. Regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 71 83