--- layout: fc_discuss_archives title: Message 93 from Frama-C-discuss on May 2010 ---
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>