--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2009 ---
Sorry, my answer was unclear: calling coq within gwhy *DOES NOT WORK* The proper way to use coq for discharging VCs generated with frama-C/jessie is frama-c -jessie-analysis -jessie-atp coq <file>.c coqide <file>.jessie/coq/<file>_why.v - Claude PS: by the way, please notice that the language for Frama-C public discussion list is english ______________________________________________________________________________________________________ Answer: Sorry for not using English language, I forgot. I tried what you tell me and I had another type of error. I am not sure whether it was necessary to put the two lines as a result or not. When I tested the two lines, I get: When I tested the first line, I get: However, I put the Coq libraries in the Variable Environment... So, I do not understand the problem and I do not find a answer to resolve this problem. Thank for your interest... Emilie -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0001.htm -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: non disponible Type: image/gif Taille: 9453 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0002.gif -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: non disponible Type: image/gif Taille: 6933 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0003.gif