--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plateform Why-2.31



Please ignore the warnings about PVS, and also about the Coq library 
Floats : the latter is superseded by Flocq, that you already have.

- Claude


On 07/25/2012 02:46 PM, DAHAN Mickael wrote:
>
> During the installation of Why-2.31  the following problems appear:
>
> ...
>
> checking Coq version... 8.3pl4
>
> checking Coq floating-point library... yes
>
> checking Coq legacy floating-point library... no
>
> checking for why3... why3
>
> checking Coq realizations for Why3... yes
>
> checking for pvs... /sbin/pvs
>
> File descriptor 5 (/home/Perco/Users/dahan/why-2.31/config.log) leaked 
> on pvs invocation. Parent PID 733: /bin/sh
>
> File descriptor 6 (/dev/pts/6) leaked on pvs invocation. Parent PID 
> 733: /bin/sh
>
> File descriptor 7 (/dev/pts/6) leaked on pvs invocation. Parent PID 
> 733: /bin/sh
>
>   /dev/mapper/control: open failed: Permission denied
>
>   Failure to communicate with kernel device-mapper driver.
>
>   WARNING: Running as a non-root user. Functionality may be unavailable.
>
> pvs: invalid option -- 'w'
>
>   Error during parsing of command line.
>
> configure: WARNING: PVS found but pvs -where did not work
>
> checking for mizf... no
>
> configure: WARNING: Cannot find Mizar.
>
> configure: creating ./config.status
>
> config.status: creating Makefile
>
> config.status: creating bench/bench
>
>                  Summary
>
> -----------------------------------------
>
> OCaml version : 3.12.0
>
> OCaml library path : /usr/lib64/ocaml
>
> OcamlGraph lib :  in Ocaml lib, subdir ocamlgraph
>
> Verbose make : no
>
> Inference of annotations : no
>
> Frama-C plugin : yes
>
>     Frama-C version : Nitrogen-20111001
>
> GWhy : yes
>
> Coq support : yes
>
>     Version : v8.1 (8.3pl4)
>
>     Lib : /usr/local/lib/coq
>
>    FP lib (Flocq) : yes
>
>     FP lib (Float) : no (Coq library AllFloat.vo not found)
>
> PVS support : no
>
> Mizar support : no
>
> Other provers support : at run-time (use why-config to configure)
>
> *Moreover, I can't find **on internet****"coq library AllFloat.vo " .*
>
> [@@THALES GROUP RESTRICTED@@]
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120726/8c4c1572/attachment.html>