--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 11



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> wrote:

> Send Frama-c-discuss mailing list submissions to
>         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
>
> You can reach the person managing the list at
>         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>
> To: 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>
> 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>> 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: 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>>
> >     To: Frama-C public discussion <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>>
> >     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>>
> >     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>
> >     > 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>>
> >     To: 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>>
> >     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>", 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>
> >     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
> > 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 ORSAY Cedex                    |
>
>
> ------------------------------
>
> Message: 2
> Date: Mon, 18 Jul 2016 09:11:13 +0200
> From: Claude Marché <Claude.Marche at inria.fr>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Installing Jessie plugin
> Message-ID: <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 ORSAY Cedex                    |
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> 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
> ***********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160719/fcc59812/attachment-0001.html>