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



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!