| Anonymous | Login | Signup for a new account | 2019-08-17 13:52 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
| 0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 15:57 | 2016-12-16 15:58 | ||||||||
| Reporter | jens | ||||||||||||
| Assigned To | correnson | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Platform | OS | OS Version | |||||||||||
| Product Version | Frama-C 14-Silicon | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0002263: Why3 warning | ||||||||||||
| Description | 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. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files | |||||||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0006324) jens (reporter) 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 |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2016-12-16 15:57 | jens | New Issue | |
| 2016-12-16 15:57 | jens | Status | new => assigned |
| 2016-12-16 15:57 | jens | Assigned To | => correnson |
| 2016-12-16 15:58 | jens | Note Added: 0006324 | |
|
Issue History |
| Copyright © 2000 - 2019 MantisBT Team |
|