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

[Frama-c-discuss] Combining Simplify and Coq



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