--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how does coq work with automatic provers?



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>