--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] loading coq scripts in Frama-C



Thanks a lot Jens and Loic !

On Mon, Oct 5, 2020 at 11:03 AM Mohit Tekriwal <tmohit at umich.edu> wrote:

> I start Coq from the Frama-C GUI. I click on the yellow bubble to load the
> Coq script in the Coq IDE and prove the goal there.
>
> On Mon, Oct 5, 2020 at 10:41 AM Mohit Tekriwal <tmohit at umich.edu> wrote:
>
>> Hello,
>>
>> I am trying to load coq scripts in Frama-C, but I have been facing
>> issues. I am using the WP plugin on the Frama-C potassium version with Coq
>> 8.9.1.
>>
>> Specifically, the problem arises when I try to prove the goal generated
>> in the Coq template generated from Frama-C. I define lemmas outside the
>> goal and import some standard Coq libraries to complete the proof. Even
>> though I am able to prove the goal in Coq, closing the coq interface does
>> not turn the yellow bubble to green in the WP goals.
>>
>> Does someone have any idea as to where I am going wrong? I would
>> appreciate the suggestions.
>>
>> Thanking you,
>>
>> Mohit Tekriwal
>>
>> --
>> Mohit Tekriwal,
>> PhD Candidate,
>> Department of Aerospace Engineering,
>> University of Michigan.
>>
>
>
> --
> Mohit Tekriwal,
> PhD Candidate,
> Department of Aerospace Engineering,
> University of Michigan.
>


-- 
Mohit Tekriwal,
PhD Candidate,
Department of Aerospace Engineering,
University of Michigan.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20201006/96562d5c/attachment.html>