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] Frama-c-discuss Digest, Vol 109, Issue 4

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 109, Issue 4
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Tue, 18 Jul 2017 14:27:49 +0000
  • In-reply-to: <mailman.31088.1500383915.1676.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.31088.1500383915.1676.frama-c-discuss@lists.gforge.inria.fr>
Hello,

to answer Jochen’s question that he accidentally posted to the mailing list (and therefore in German.)

>    CVC3 nur fuer diejenigen Faelle aufgerufen, in denen Alt-Ergo keinen 
>   Beweis gefunden hat?

No,  all  provers received all prover obligations that Qed could not discharge.
That is the difference between the results in appendices A.2 and A3.
  
>    Und warum sind die Zahlen so klein? Allein push-heap muesste doch knapp 
>   100 Proof Obligations gehabt haben, und fuer das ganze "ACSL by Example" 
>    wuerde ich spontan ca. 1000 erwarten - ? Kann der Qed ca. 900 davon 
>    schon alleine loesen?

The numbers refer to algorithms not proof obligations!
I think you missed that point.

Jens