--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2010 ---
Hello, I'm trying to prove some C functions with frama-c. Some of the VCs could be automatically proved by some ATP (e.g. Simplify), but some can't. For the remaining VCs, I'd like to use Coq. I proved the first VCs with Simplify: frama-c -jessie-analysis -jessie-atp simplify file.c This gives me an output such as "total: 4, valid: 2, unknown: 2" Now for the remaining VCs I planned to prove with Coq, I know I can use: frama-c -jessie-analysis -jessie-atp coq file.c This creates a file file.jessie/coq/file_why.v, which I can open with the coqide, and start filling in the proves. My question now is: Is there a way to combine simplify and coq, to get a file_why.v where some of the proofs are already filled in (those that can be proved by simplify)? Regards Michael