--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2010 ---
Thanks for the tip. Helped a lot. One minor modification which I hope doesn't change the behavior of the command. I used -jessie-analysis option instead of -jessie. This version of Coq seems to not know about -jessie option. frama-c -jessie -jessie-atp coq fbmove.c frama-c: unknown option `-jessie'. toplevel options files... On Thu, Jan 7, 2010 at 10:38 AM, Claude Marche <Claude.Marche at inria.fr> wrote: > > to use coq within Frama-C/Jessie, you cannot use gwhy. Instead > > ? frama-c -jessie -jessie-atp coq file.c > > should generate > > ? file.jessie/coq/file_why.v > > and you can fill-in proofs as usual with Coq, e.g > > coqide file.jessie/coq/file_why.v > > - claude > > Groleo Marius wrote: >> Hi, >> I have coq 8.2 and why 2.18 on ubuntu 9.10. >> >> When I try to prove some code with coq, I get the following message in >> the console. >> Thread 1 killed on uncaught exception Failure("For interactive >> provers, option --project must be set") >> >> How can I get around this issue ? >> >> Thanks. >> > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Regards, Groleo!