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



Hi,

As you said, though it has given warning, proof obligations are discharged
successfully.

Thanks,

Prasuna


On Tue, Jul 19, 2016 at 6:02 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 11 (Mohamed Iguernlala)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 19 Jul 2016 14:32:07 +0200
> From: Mohamed Iguernlala <iguer.auto at gmail.com>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue
>         11
> Message-ID: <88937310-77db-2edf-d1c7-7883d694d409 at gmail.com>
> Content-Type: text/plain; charset="utf-8"; Format="flowed"
>
> 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.html
> >
>
> ------------------------------
>
> 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 13
> ***********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160722/ff38dce3/attachment-0001.html>