--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2016 ---
Hi, I guess you get something like: "Warning: prover Alt-Ergo version 1.01 is not known to be supported." This doesn't mean that the version is not supported. You have to try to make a proof to see if the translation of proof obligations to the "possibly unsupported" version, and if the parsing of prover's answer work well. Regards, - Mohamed. Le 19/07/2016 à 11:46, Prasuna Saka a écrit : > > Mr. Claude, > > Thanks for your helpful note on my queries. Now I think I have more or > less done with the installation. As you said, I have done the following: > > > -- Installed opam > -- opam install ocaml > -- opam install why > > with the above commands, > > ocaml version 4.02.3, > FRAMA-C version sodium-20150201 > why3 version 0.85 > have got installed successfully. I could launch the GUI as well ( > with the command frama-c -jessie testpgm.c).Since no provers are > installed a message to run why3 congig --detect-provers is popped. > > I have installed Alt-Ergo SMT solver using the command "opam install > alt-ergo". Then, alt-ergo version 0.991 version has got installed. > > With the command why3 config --detect then, > > this it shown that this version of alt-ergo is not supported. > Same is happening with the coq Prover as well. > > How do I find which version of the external provers will be supported > by my current configuration.? Do I need to install all the provers > with opam or can I use sudo apt-get install command? > > I wanted to work with Coq prover , as I have a C Program involving > floats and trigonometric functions to be verified. > > > Thanks & Regards > > Prasuna > > > > > > > On Mon, Jul 18, 2016 at 3:30 PM, > <frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr>> wrote: > > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr> > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > <mailto:frama-c-discuss-owner at lists.gforge.inria.fr> > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Re: Frama-c-discuss Digest, Vol 97, Issue 9 (Claude Marché) > 2. Re: Installing Jessie plugin (Claude Marché) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 18 Jul 2016 09:09:30 +0200 > From: Claude Marché <Claude.Marche at inria.fr > <mailto:Claude.Marche at inria.fr>> > To: frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 9 > Message-ID: <578C80AA.8040500 at inria.fr > <mailto:578C80AA.8040500 at inria.fr>> > Content-Type: text/plain; charset=utf-8 > > > Dear Prasuna, > > I must admit I don't understand your problem. with a fresh opam > installation simply typing > > opam install why > > should install everything needed, including the dependencies > Frama-C and > why3. > > I wonder if you are not trying to install why3 again after installing > why: this is wrong, you should not do that. Why depend on Why3, > not the > other way around. > > Otherwise, please try to report the problem more clearly with a > detailed > log of what happens for you. > > - Claude > > Le 15/07/2016 15:17, Prasuna Saka a écrit : > > Hi, > > > > Thhnks for the reply > > > > If I install why and why3 with opam , provided ocaml is > installed using > > spam then latest why3 version- why3-0.87 is installed which is not > > supported by the FRAMA_C version i am having. How do I really > install > > the required why3 and why version using opam. > > > > Hope my question is clear. > > > > I have tried to install everything in the other way as well, i.e > without > > using opam: > > > > Firstly, ocaml version 4.02.3 is installed and when why3-0.83 is > tried > > for installing, error thrown for the make command. > > > > Do not know what to do now! > > > > > > Thanks > > Prasuna > > > > On Fri, Jul 15, 2016 at 3:30 PM, > > <frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr> > > <mailto:frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr>>> wrote: > > > > Send Frama-c-discuss mailing list submissions to > > frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > > <mailto:frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr>> > > > > To subscribe or unsubscribe via the World Wide Web, visit > > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > or, via email, send a message with subject or body 'help' to > > frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr> > > <mailto:frama-c-discuss-request at lists.gforge.inria.fr > <mailto:frama-c-discuss-request at lists.gforge.inria.fr>> > > > > You can reach the person managing the list at > > frama-c-discuss-owner at lists.gforge.inria.fr > <mailto:frama-c-discuss-owner at lists.gforge.inria.fr> > > <mailto:frama-c-discuss-owner at lists.gforge.inria.fr > <mailto:frama-c-discuss-owner at lists.gforge.inria.fr>> > > > > When replying, please edit your Subject line so it is more > specific > > than "Re: Contents of Frama-c-discuss digest..." > > > > > > Today's Topics: > > > > 1. Re: Dependency of ocaml version on why3-0.83 (Boris > Yakobowski) > > 2. Installing Jessie plugin (Prasuna Saka) > > > > > > > ---------------------------------------------------------------------- > > > > Message: 1 > > Date: Thu, 14 Jul 2016 15:21:43 +0200 > > From: Boris Yakobowski <boris at yakobowski.org > <mailto:boris at yakobowski.org> > > <mailto:boris at yakobowski.org <mailto:boris at yakobowski.org>>> > > To: Frama-C public discussion > <frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > > <mailto:frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr>>> > > Subject: Re: [Frama-c-discuss] Dependency of ocaml version on > > why3-0.83 > > Message-ID: > > > > > <CABbVA-D=8yoc4e1kB0dzqVyaLs5GKFL-pKAm=h9ueuyU3vTCGQ at mail.gmail.com > <mailto:h9ueuyU3vTCGQ at mail.gmail.com> > > <mailto:h9ueuyU3vTCGQ at mail.gmail.com > <mailto:h9ueuyU3vTCGQ at mail.gmail.com>>> > > Content-Type: text/plain; charset="utf-8" > > > > Hi, > > > > It seems you have used Opam to install OCaml. You should do > the same > > thing > > for Jessie and Why3, by installing respectively the why and why3 > > packages. > > If you are not root, install your own version of Opam. It > will make > > things > > simpler in the end. > > > > HTH, > > > > On Thu, Jul 14, 2016 at 8:17 AM, Prasuna Saka > > <prasuna.drdo at gmail.com <mailto:prasuna.drdo at gmail.com> > <mailto:prasuna.drdo at gmail.com <mailto:prasuna.drdo at gmail.com>>> > > wrote: > > > > > Hi, > > > > > > I am having FRAMA-C Version:Neon-20140301 installed. Want > to install > > > Jessie Plug-in. As per the dependency tree listed in the > web page of > > > Krakatoa and Jessie , compatible Why version is 2.34, > which got > > installed > > > successfully. However, when trying to install Why3-0.83 , > > following error > > > is thrown: > > > > > > Output of running configure command: > > > > > > Verbose make : no > > > OCaml compiler : yes > > > Version : 4.02.3 > > > Library path : /root/.opam/4.02.3/lib/ocaml > > > Native compilation : yes > > > Profiling : no > > > Zarith : yes > > > IDE : yes > > > Bench tool : no (sqlite3 not found) > > > Documentation : no (rubber not found) > > > Coq support : no (version is 8.5pl2 but need > version > > 8.4 or > > > higher) > > > PVS support : no (pvs not found) > > > Isabelle support : no (isabelle not found) > > > Frama-C support : no (disabled by default) > > > Hypothesis selection : yes > > > Installable : yes > > > Binary path : ${exec_prefix}/bin > > > Lib path : ${exec_prefix}/lib/why3 > > > Data path : ${prefix}/share/why3 > > > Ocaml Library : /root/.opam/4.02.3/lib/why3 > > > Relocatable : no > > > > > > Error with make command: > > > > > > Error: src/util/debug.cmi > > > is not a compiled interface for this version of OCaml. > > > It seems to be for an older version of OCaml. > > > Makefile:1685: recipe for target > 'src/driver/call_provers.cmx' failed > > > make: *** [src/driver/call_provers.cmx] Error 2 > > > > > > May I please know what is this error for and how to > resolve it? > > > > > > Thanks > > > Prasuna > > > > > > _______________________________________________ > > > Frama-c-discuss mailing list > > > Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > > <mailto:Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr>> > > > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > > > > > > > > > -- > > Boris > > -------------- next part -------------- > > An HTML attachment was scrubbed... > > URL: > > > <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160714/30c4b470/attachment-0001.html> > > > > ------------------------------ > > > > Message: 2 > > Date: Fri, 15 Jul 2016 15:10:27 +0530 > > From: Prasuna Saka <prasuna.drdo at gmail.com > <mailto:prasuna.drdo at gmail.com> > > <mailto:prasuna.drdo at gmail.com <mailto:prasuna.drdo at gmail.com>>> > > To: frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > > <mailto:frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr>> > > Subject: [Frama-c-discuss] Installing Jessie plugin > > Message-ID: > > > > > <CAA80GKO364LP85DZw9kG=MnzB748ftseUDSq_WvP6zd5Zu-vxQ at mail.gmail.com > <mailto:MnzB748ftseUDSq_WvP6zd5Zu-vxQ at mail.gmail.com> > > <mailto:MnzB748ftseUDSq_WvP6zd5Zu-vxQ at mail.gmail.com > <mailto:MnzB748ftseUDSq_WvP6zd5Zu-vxQ at mail.gmail.com>>> > > Content-Type: text/plain; charset="utf-8" > > > > Having FRAMAC Neon version installed, trying to install > jessie plug-in, > > getting into the following problem. > > > > Chosen Why3-0.83 and why2-35. > > > > While installing why3, following is the issue: > > > > output of configure command is : > > > > Verbose make : no > > OCaml compiler : yes > > Version : 4.02.3 > > Library path : /usr/local/lib/ocaml > > Native compilation : yes > > Profiling : no > > Zarith : no (zarith not found) > > IDE : no (lablgtk2 not found) > > Bench tool : no (sqlite3 not found) > > Documentation : no (rubber not found) > > Coq support : yes > > Version : 8.4pl4 > > Library path : /usr/lib/coq > > "why3" tactic : no (/usr/lib/coq/kernel/term.cmi > not found) > > Realization support : yes > > FP arithmetic : no (Flocq >= 2.2 not found) > > PVS support : no (pvs not found) > > Isabelle support : no (isabelle not found) > > Frama-C support : no (disabled by default) > > Hypothesis selection : no (ocamlgraph not found) > > Installable : yes > > Binary path : ${exec_prefix}/bin > > Lib path : ${exec_prefix}/lib/why3 > > Data path : ${prefix}/share/why3 > > Ocaml Library : /usr/local/lib/ocaml/why3 > > Relocatable : no > > > > With make command, following is the error thrown: > > > > File "src/driver/call_provers.ml <http://call_provers.ml> > <http://call_provers.ml>", line 1: > > Error: src/util/debug.cmi > > is not a compiled interface for this version of OCaml. > > It seems to be for an older version of OCaml. > > Makefile:1685: recipe for target > 'src/driver/call_provers.cmx' failed > > make: *** [src/driver/call_provers.cmx] Error 2 > > > > Please, help me out to solve this. > > > > Regards, > > Prasuna > > -------------- next part -------------- > > An HTML attachment was scrubbed... > > URL: > > > <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160715/5dbf5771/attachment-0001.html> > > > > ------------------------------ > > > > Subject: Digest Footer > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > > <mailto:Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr>> > > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > > ------------------------------ > > > > End of Frama-c-discuss Digest, Vol 97, Issue 9 > > ********************************************** > > > > > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > > -- > Claude Marché | tel: +33 1 69 15 66 08 > INRIA Saclay - Ãle-de-France | > Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 <http://www.lri.fr/%7Emarche/%0AF-91405> ORSAY Cedex > | > > > ------------------------------ > > Message: 2 > Date: Mon, 18 Jul 2016 09:11:13 +0200 > From: Claude Marché <Claude.Marche at inria.fr > <mailto:Claude.Marche at inria.fr>> > To: frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] Installing Jessie plugin > Message-ID: <578C8111.2070706 at inria.fr > <mailto:578C8111.2070706 at inria.fr>> > Content-Type: text/plain; charset=utf-8 > > > > Le 15/07/2016 11:40, Prasuna Saka a écrit : > > Having FRAMAC Neon version installed, trying to install jessie > plug-in, > > getting into the following problem. > > > > Chosen Why3-0.83 and why2-35. > > please be careful with the dependencies : see http://krakatoa.lri.fr/ > > however, as I said before with opam the proper dependencies should be > chosen for you. > > - Claude > > > > -- > Claude Marché | tel: +33 1 69 15 66 08 > INRIA Saclay - Ãle-de-France | > Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 <http://www.lri.fr/%7Emarche/%0AF-91405> ORSAY Cedex > | > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > ------------------------------ > > End of Frama-c-discuss Digest, Vol 97, Issue 11 > *********************************************** > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160719/282c2ce8/attachment-0001.html>