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

  • Subject: [Frama-c-discuss] Plateform Why-2.31
  • From: mickael.dahan at thalesgroup.com (DAHAN Mickael)
  • Date: Wed, 25 Jul 2012 14:46:02 +0200
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@@]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120725/8a0563fb/attachment.html>