--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] GWhy not working with Coq.



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.
>