Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002263Frama-CPlug-in > wppublic2016-12-16 15:572016-12-16 15:58
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002263: Why3 warning
DescriptionWhen 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.
TagsNo tags attached.
Attached Files

- 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

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker