--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on August 2017 ---
It seems that compilation of Why by opam did not produce the Jessie plugin. Unfortunately I don't know how to get the opam log of a successfully installed opam package. I suggest to compile the sources directly instead and see what happens: download http://why.lri.fr/download/why-2.38.tar.gz and then tar zxvf why-2.38.tar.gz cd why-2.38 ./configure and send the output if it says it will compile the frama-c plugin then try make and send the output - Claude Le 22/08/2017 à 10:22, Junkil âDavidâ Park a écrit : > Thanks Julien for your quick reply. > > The following output log shows the error message. Do you have any thought? By the way, I tried to install "why" a couple of times on fresh opam switches. > > ~ â¯â¯â¯ opam list > # Installed packages for 4.03.0: > alt-ergo 1.30 Alt-Ergo, an SMT Solver for Software Verification > base-bigarray base Bigarray library distributed with the OCaml compiler > base-num base Num 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 > camlzip 1.07 Provides easy access to compressed files in ZIP, GZIP and JAR format > 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 > depext 1.0.5 Query and install external dependencies of OPAM packages > frama-c 20161101 Platform dedicated to the analysis of source code written in C. Silicon version. > frama-c-base 20161101 Platform dedicated to the analysis of source code written in C. Silicon version. > lablgtk 2.18.5 OCaml interface to GTK+ > menhir 20170712 LR(1) parser generator > num 0 The Num library for arbitrary-precision integer and rational arithmetic > ocamlbuild 0.11.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. > ocamlfind 1.7.3 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 solving systems of linear inequalities and optimizing linear objective functions > why 2.38 Why is a software verification platform. > why3 0.87.3 Why3 environment for deductive program verification. > why3-base 0.87.3 Why3 environment for deductive program verification (base) > zarith 1.5 Implements arithmetic and logical operations over arbitrary-precision integers > > > ~ â¯â¯â¯ frama-c -kernel-msg-key dynlink -jessie > [kernel:dynlink] plugin_dir: /Users/david/.opam/4.03.0/lib/frama-c/plugins > [kernel:dynlink] Loading directory '/Users/david/.opam/4.03.0/lib/frama-c/plugins' > [kernel:dynlink] setting findlib path to /Users/david/.opam/4.03.0/lib/frama-c/plugins > [kernel:dynlink] trying to load frama-c-aorai frama-c-callgraph frama-c-constant_propagation > frama-c-from frama-c-impact frama-c-inout > frama-c-loopanalysis frama-c-metrics frama-c-nonterm > frama-c-obfuscator frama-c-occurrence frama-c-pdg > frama-c-postdominators frama-c-print_api frama-c-report > frama-c-rtegen frama-c-scope frama-c-security_slicing > frama-c-slicing frama-c-sparecode frama-c-users frama-c-value > frama-c-variadic frama-c-wp > [kernel:dynlink] Loading module 'frama-c-aorai' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Aorai.cmxs'. > [kernel:dynlink] Loading module 'frama-c-callgraph' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Callgraph.cmxs'. > [kernel:dynlink] Loading module 'frama-c-loopanalysis' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/LoopAnalysis.cmxs'. > [kernel:dynlink] Loading module 'frama-c-value' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Value.cmxs'. > [kernel:dynlink] Loading module 'frama-c-constant_propagation' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Constant_Propagation.cmxs'. > [kernel:dynlink] Loading module 'frama-c-from' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/From.cmxs'. > [kernel:dynlink] Loading module 'frama-c-inout' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Inout.cmxs'. > [kernel:dynlink] Loading module 'frama-c-pdg' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Pdg.cmxs'. > [kernel:dynlink] Loading module 'frama-c-impact' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Impact.cmxs'. > [kernel:dynlink] Loading module 'frama-c-metrics' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Metrics.cmxs'. > [kernel:dynlink] Loading module 'frama-c-nonterm' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Nonterm.cmxs'. > [kernel:dynlink] Loading module 'frama-c-obfuscator' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Obfuscator.cmxs'. > [kernel:dynlink] Loading module 'frama-c-occurrence' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Occurrence.cmxs'. > [kernel:dynlink] Loading module 'frama-c-postdominators' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Postdominators.cmxs'. > [kernel:dynlink] Loading module 'frama-c-print_api' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Print_api.cmxs'. > [kernel:dynlink] Loading module 'frama-c-report' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Report.cmxs'. > [kernel:dynlink] Loading module 'frama-c-rtegen' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/RteGen.cmxs'. > [kernel:dynlink] Loading module 'frama-c-scope' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Scope.cmxs'. > [kernel:dynlink] Loading module 'frama-c-security_slicing' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Security_slicing.cmxs'. > [kernel:dynlink] Loading module 'frama-c-slicing' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Slicing.cmxs'. > [kernel:dynlink] Loading module 'frama-c-sparecode' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Sparecode.cmxs'. > [kernel:dynlink] Loading module 'frama-c-users' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Users.cmxs'. > [kernel:dynlink] Loading module 'frama-c-variadic' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Variadic.cmxs'. > [kernel:dynlink] Loading module 'frama-c-wp' from '/Users/david/.opam/4.03.0/lib/frama-c/plugins/top/Wp.cmxs'. > [kernel] user error: option `-jessie' is unknown. > use `frama-c -help' for more information. > [kernel] Frama-C aborted: invalid user input. > > > Thanks, > Junkil > >> On Aug 22, 2017, at 4:16 AM, Julien Signoles <Julien.Signoles at cea.fr> wrote: >> >> Le 22/08/2017 10:15, Julien Signoles a écrit : >>> $ frama-c -kernel-msg-key dynling <other options and files> >> >> Sorry, read "dynlink" instead of "dynling" >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |