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 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>