--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on August 2017 ---
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