--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2020 ---
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>