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] Plateform Why3 0.72

During the installation of Why3 O.72  the following problems appear:

typed commands:

tar -xvzf why3-0.72.tar.gz

cd why3-0.72

./configure --enable-coq-plugin --enable-coq-libs

make


results:

                 Summary
-----------------------------------------
OCaml version           : 3.12.0
OCaml library path      : /usr/lib64/ocaml
Compile in native code  : yes
Verbose make            : no
Why IDE                 : yes
Why bench tool          : no
Why documentation       : no
Coq support             : yes
    Version             : 8.4beta2
    Lib                 : /usr/local/lib/coq
    Plugin support      : yes
    Realization support : yes
        FP arithmetic   : yes
hypothesis selection    : yes
debugging symbols       : no
profiling               : no
localdir                : no




...
Ocamlopt src/ide/gconfig.ml
Ocamlopt src/ide/gmain.ml
Linking  bin/why3ide.opt
Ocamlopt src/ide/replay.ml
Linking  bin/why3replayer.opt
Ocamlc   src/why3session/why3session_lib.mli
Ocamlopt src/why3session/why3session_lib.ml
Ocamlopt src/why3session/why3session_copy.ml
Ocamlopt src/why3session/why3session_info.ml
Ocamlopt src/why3session/why3session_latex.ml
Ocamlopt src/why3session/why3session_html.ml
Ocamlopt src/why3session/why3session_rm.ml
Ocamlopt src/why3session/why3session.ml
Linking  bin/why3session.opt
Ocamlopt src/coq-tactic/why3tac.ml
File "src/coq-tactic/why3tac.ml", line 477, characters 14-20:
Error: This pattern matches values of type 'a option
       but a pattern was expected which matches values of type
         Declarations.constant_def
make: *** [src/coq-tactic/why3tac.cmx] Error 2





[@@THALES GROUP RESTRICTED@@]

De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Claude Marche
Envoy? : vendredi 20 juillet 2012 21:13
? : frama-c-discuss at lists.gforge.inria.fr
Objet : Re: [Frama-c-discuss] Plateform Why3 0.72

On 07/20/2012 10:20 AM, DAHAN Mickael wrote:
Hello.

I would like to know how can I do to launch the plateform Why3 0.72 on frama-c Nitrogen.


The formulation of your question is somewhat strange... Please see http://krakatoa.lri.fr for explanations on the relations between Frama-C, Why3, and the Jessie plugin. In short:

* compile and install Frama-C Nitrogen and Why3 in any order (the newer Why3 0.73 if possible ;-)
* compile and install Why 2.31 which contains the Jessie plugin
* detect provers: why3config --detect

then:

frama-c -jessie file.c

will start compute VCs for your C code and start the why3 GUI on them

- Claude
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120723/32b96069/attachment.html>