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

[Frama-c-discuss] Generate Coq file using Frama-c / Why



Hi everyone,

to continue on this topic of extracting a coq file from a C file using Frama-C/Jessie/Why, 
I wanted to share with you a small script that produces a file for a given obligation.

The matter was that the coq goal via jessie-atp provides a file with all the proof obligations, which could be huge.

The script is available at http://cavale.gforge.enseeiht.fr/files/extract_obligation

It takes the sources, a function name and an obligation name (which could be obtained from the Frama-c gui) and produces either a coq file, a why file for alt-ergo or an smtlib file.

Hoping it could be of interest for one of you,

Best regards,

pl
-- 
Pierre-Lo?c Garoche
pierre-loic.garoche at onera.fr
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100526/49695789/attachment.pgp>