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

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                    |