--- layout: fc_discuss_archives title: Message 26 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



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                    |