Frama-C Bug Tracking System - Frama-C
View Issue Details
0002263Frama-CPlug-in > wppublic2016-12-16 15:572016-12-16 15:58
jens 
correnson 
normalminoralways
assignedopen 
Frama-C 14-Silicon 
 
0002263: Why3 warning
When running WP I observe the following warning [Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14: Library file not found: int The problem occurs both under Linux and macOS.
No tags attached.
Issue History
2016-12-16 15:57jensNew Issue
2016-12-16 15:57jensStatusnew => assigned
2016-12-16 15:57jensAssigned To => correnson
2016-12-16 15:58jensNote Added: 0006324

Notes
(0006324)
jens   
2016-12-16 15:58   
My Frama-C install (through opam) looks like this # Installed packages for 4.04.0: alt-ergo 1.30 Alt-Ergo, an SMT Solver for Software Verification base-bigarray base Bigarray library distributed with the OCaml compiler base-threads base Threads library distributed with the OCaml compiler base-unix base Unix library distributed with the OCaml compiler camlp5 6.17 Preprocessor-pretty-printer of OCaml camlzip 1.06 Provides easy access to compressed files in ZIP, GZIP and JAR format cmdliner 0.9.8 Declarative definition of command line interfaces for OCaml conf-autoconf 0.1 Virtual package relying on autoconf installation. conf-gmp 1 Virtual package relying on a GMP lib system installation. conf-gnomecanvas 2 Virtual package relying on a Gnomecanvas system installation. conf-gtksourceview 2 Virtual package relying on a GtkSourceView system installation. conf-m4 1 Virtual package relying on m4 conf-perl 1 Virtual package relying on perl conf-which 1 Virtual package relying on which coq 8.5.3 Formal proof management system. coqide 8.5.3 IDE of the Coq formal proof management system. depext 1.0.2 Query and install external dependencies of OPAM packages frama-c 20161101 Platform dedicated to the analysis of source code written in C. Silico frama-c-base 20161101 Platform dedicated to the analysis of source code written in C. Silico lablgtk 2.18.5 OCaml interface to GTK+ menhir 20161115 LR(1) parser generator ocamlbuild 0.9.3 OCamlbuild is a build system with builtin rules to easily build most O ocamlfind 1.7.1 A library manager for OCaml ocamlgraph 1.8.7 A generic graph library for OCaml ocplib-simplex 0.3 A library implementing a simplex algorithm, in a functional style, for why3 0.87.2 Why3 environment for deductive program verification. why3-base 0.87.2 Why3 environment for deductive program verification (base) zarith 1.4.1 Implements arithmetic and logical operations over arbitrary-precision