--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on July 2012 ---
[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>