--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] information for proof seems to get lost



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