--- layout: fc_discuss_archives title: Message 20 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



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>