--- layout: fc_discuss_archives title: Message 94 from Frama-C-discuss on May 2010 ---
Hello Pierre-Lo?c, Pierre-Lo?c Garoche a ?crit : > 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, Many thanks for your contribution. Maybe could you put this file (or a link to this file) somewhere on the Frama-C wiki (http://bts.frama-c.com/dokuwiki/doku.php?id=mantis%3AFrama-C%3Astart)? br, Julien