--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on August 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [PROVENANCE INTERNET] Re: [Why-discuss] Installing Jessie



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