how to use coq with frama-c
ID0000872: This issue was created automatically from Mantis Issue 872. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000872 | Frama-C | Plug-in > jessie | public | 2011-06-25 | 2011-07-25 |
| Reporter | luoting | Assigned To | cmarche | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
hello,
firstly, I run "frama-c -jessie max.c",and then a file max.why has been generated. secondly, run why --coq max.why. the shell shows "unbound type 'bitvector'".Why?
I have used automatic theorem verifier ,and all verification conditions have been discharged. why an error happens when use coq?
If all verification conditions are not discharged, is it right to run "why --coq .why" to discharge the left condition?
The lemmas should be verified first by coq, and then can be used by automatic prover.yes? if yes ,how can the coq proved result be transmited to the automatic provers?
Thanks!