--- layout: fc_discuss_archives title: Message 94 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



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