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] how does coq work with automatic provers?

  • Subject: [Frama-c-discuss] how does coq work with automatic provers?
  • From: luoting8609 at 163.com (罗婷)
  • Date: Mon, 27 Jun 2011 16:17:50 +0800 (CST)
hello,
  I have specified a C source programme(e.g max.c) with ACSL, and then run   frama-c -jessie max.c  . The gc why launched and vcs generated . I plan to use automatic prover and coq to discharge all vcs. however , max.c is a simple example and all vcs are discharged automaticlly. but I still want to know how to verify by coq. so I run why --coq max.why(max.why is generated after running frama-c -jessie max.c). the shell shows "unbound type 'bitvector'".Why? 
    If all verification conditions are not discharged, is it right to run "why --coq .why" to discharge the left condition?
  Sometimes, lemmas should be added to help the proving process.The lemmas should be verified first by coq, but how can coq tell other provers the lemmas have been proved to be right,that is how can the coq proved result be transmited to the automatic provers? If lemmas were added and some vcs were not automaticlly discharged, the proving sequence should be ,first coq ,then automatic prover, lastly coq?
      Thank you for your kindness ! Best wishes!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110627/d615c5f6/attachment.htm>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: max.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110627/d615c5f6/attachment.txt>