Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- Subject: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Tue, 05 Nov 2013 14:48:13 +0100
- In-reply-to: <op.w500cxf51b2obh@novo.act-europe.fr>
- References: <CAP6nMJSdSknD8vZDppXi0aNz55zmyi_98ajThBmcMOn3Buks7Q@mail.gmail.com> <525F8DA9.4080702@inria.fr> <op.w50nqod91b2obh@novo.act-europe.fr> <CAP6nMJRdZ1nZHZxh4mF54UL_SVJ6_fjFbUrPvzKdgGwc-H52cg@mail.gmail.com> <op.w500cxf51b2obh@novo.act-europe.fr>
Le 04/11/2013 14:13, Johannes Kanig a ?crit : > Hi Nanci, > > On Mon, 04 Nov 2013 13:28:40 +0100, Nanci Naomi <nnarai at gmail.com> wrote: >> We have not tried to run the David's suggestion, because we are Frama-C >> begginer's users and we do not know how to modify the makefiles. However, >> if you could give the hints to do that, we can send you the file. > > Actually, my e-mail was mis-guided, and there is no problem here. As > Claude explained in this thread (but I discovered his message only > later), the number of VCs is expected here. > > You may want to see with the authors of the Jessie plugin if the fastwp > can be activated now. There is no easy way to activate Why3's fastwp from Jessie for the moment. If you want to experiment with that, you have to dig into the generated makefile (in file.jessie/file.makefile, look for the call to why3ide and add the option manually) This should be available in future release - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |
- References:
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: kanig at adacore.com (Johannes Kanig)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: nnarai at gmail.com (Nanci Naomi)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: kanig at adacore.com (Johannes Kanig)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- Prev by Date: [Frama-c-discuss] how jessie and why platform work to generate a .v output?
- Next by Date: [Frama-c-discuss] how jessie and why platform work to generate a .v output?
- Previous by thread: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- Next by thread: [Frama-c-discuss] [Jessie] FP overflow
- Index(es):