Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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