Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] information for proof seems to get lost
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Tue, 17 Feb 2009 18:35:58 +0100
  • In-reply-to: <A7B824159A924BB6A183CC3D816C4A0E@AHARDPLACE>
  • References: <A7B824159A924BB6A183CC3D816C4A0E@AHARDPLACE>
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