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] Frama-c-discuss Digest, Vol 97, Issue 11

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 11
  • From: prasuna.drdo at gmail.com (Prasuna Saka)
  • Date: Tue, 19 Jul 2016 15:16:00 +0530
  • In-reply-to: <mailman.9.1468836006.24430.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.9.1468836006.24430.frama-c-discuss@lists.gforge.inria.fr>
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>