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

Hi,
> ./configure

x why-2.38/
x why-2.38/jc/
x why-2.38/jc/jc_effect.ml
x why-2.38/jc/jc_norm.ml
x why-2.38/jc/jc_interp.ml
x why-2.38/jc/jc_options.ml
x why-2.38/jc/jc_constructors.mli
x why-2.38/jc/output.ml
x why-2.38/jc/jc_region.ml
x why-2.38/jc/jc_poutput.ml
x why-2.38/jc/jc_lexer.mli
x why-2.38/jc/jc_pervasives.mli
x why-2.38/jc/jc_annot_fail.ml
x why-2.38/jc/jc_type_var.mli
x why-2.38/jc/jc_noutput.ml
x why-2.38/jc/jc_iterators.mli
x why-2.38/jc/jc_make.ml
x why-2.38/jc/jc_type_var.ml
x why-2.38/jc/jc_iterators.ml
x why-2.38/jc/jc_output.ml
x why-2.38/jc/jc_main.ml
x why-2.38/jc/jc_stdlib_lt312.ml
x why-2.38/jc/jc_typing.ml
x why-2.38/jc/jc_pervasives.ml
x why-2.38/jc/jc_interp_misc.mli
x why-2.38/jc/jc_common_options.mli
x why-2.38/jc/numconst.mll
x why-2.38/jc/jc_separation.ml
x why-2.38/jc/jc_stdlib_ge312.ml
x why-2.38/jc/jc_pattern.ml
x why-2.38/jc/jc_envset.mli
x why-2.38/jc/jc_lexer.mll
x why-2.38/jc/jc_ast.mli
x why-2.38/jc/output.mli
x why-2.38/jc/jc_stdlib_ge400.ml
x why-2.38/jc/jc_options.mli
x why-2.38/jc/jc_common_options.ml
x why-2.38/jc/jc_frame.ml
x why-2.38/jc/jc_parser.mly
x why-2.38/jc/jc_frame_notin.ml
x why-2.38/jc/jc_struct_tools.ml
x why-2.38/jc/jc_invariants.ml
x why-2.38/jc/jc_callgraph.ml
x why-2.38/jc/jc_constructors.ml
x why-2.38/jc/jc_norm.mli
x why-2.38/jc/jc_envset.ml
x why-2.38/jc/numconst.mli
x why-2.38/jc/jc_interp.mli
x why-2.38/jc/jc_env.mli
x why-2.38/jc/jc_annot_inference.ml
x why-2.38/jc/jc_output_misc.ml
x why-2.38/jc/jc_ai.mli
x why-2.38/jc/jc_control_flow.ml
x why-2.38/jc/jc_callgraph.mli
x why-2.38/jc/jc_frame.mli
x why-2.38/jc/jc_typing.mli
x why-2.38/jc/jc_struct_tools.mli
x why-2.38/jc/jc_name.ml
x why-2.38/jc/jc_fenv.ml
x why-2.38/jc/jc_interp_misc.ml
x why-2.38/tools/
x why-2.38/tools/regtest.ml
x why-2.38/mix/
x why-2.38/mix/mix_cfg.ml
x why-2.38/mix/mix_interp.ml
x why-2.38/mix/mix_main.ml
x why-2.38/mix/mix_seq.ml
x why-2.38/mix/mix_cfg.mli
x why-2.38/mix/test.ml
x why-2.38/mix/mix_lexer.mll
x why-2.38/mix/mix_parser.mly
x why-2.38/mix/mix_ast.mli
x why-2.38/java/
x why-2.38/java/java_syntax.ml
x why-2.38/java/java_main.ml
x why-2.38/java/java_typing.mli
x why-2.38/java/java_analysis.ml
x why-2.38/java/java_abstract.ml
x why-2.38/java/java_env.mli
x why-2.38/java/java_options.ml
x why-2.38/java/java_ast.mli
x why-2.38/java/java_tast.mli
x why-2.38/java/java_lexer.mll
x why-2.38/java/java_pervasives.ml
x why-2.38/java/java_callgraph.ml
x why-2.38/java/java_callgraph.mli
x why-2.38/java/java_typing.ml
x why-2.38/java/java_interp.ml
x why-2.38/java/java_parser.mly
x why-2.38/frama-c-plugin/
x why-2.38/frama-c-plugin/interp.ml
x why-2.38/frama-c-plugin/jessie_integer.ml
x why-2.38/frama-c-plugin/norm.mli
x why-2.38/frama-c-plugin/jessie_config.ml
x why-2.38/frama-c-plugin/interp.mli
x why-2.38/frama-c-plugin/norm.ml
x why-2.38/frama-c-plugin/retype.ml
x why-2.38/frama-c-plugin/Jessie.mli
x why-2.38/frama-c-plugin/rewrite.ml
x why-2.38/frama-c-plugin/common.ml
x why-2.38/frama-c-plugin/jessie_options.mli
x why-2.38/frama-c-plugin/jessie_options.ml
x why-2.38/frama-c-plugin/common.mli
x why-2.38/frama-c-plugin/register.ml
x why-2.38/frama-c-plugin/configure
x why-2.38/frama-c-plugin/share/
x why-2.38/frama-c-plugin/share/jessie/
x why-2.38/frama-c-plugin/share/jessie/stdlib.h
x why-2.38/frama-c-plugin/share/jessie/unistd.h
x why-2.38/frama-c-plugin/share/jessie/strings.h
x why-2.38/frama-c-plugin/share/jessie/stddef.h
x why-2.38/frama-c-plugin/share/jessie/jessie_prolog.h
x why-2.38/frama-c-plugin/share/jessie/wchar.h
x why-2.38/frama-c-plugin/share/jessie/ctype.h
x why-2.38/frama-c-plugin/share/jessie/string.h
x why-2.38/frama-c-plugin/share/jessie/jessie_exact_prolog.h
x why-2.38/frama-c-plugin/share/jessie/assert.h
x why-2.38/frama-c-plugin/share/jessie/jessie_machine_prolog.h
x why-2.38/frama-c-plugin/share/jessie/stdio.h
x why-2.38/frama-c-plugin/Makefile
x why-2.38/tests/
x why-2.38/tests/regtest.sh
x why-2.38/tests/java/
x why-2.38/tests/java/coq/
x why-2.38/tests/java/coq/Fibonacci_why.v
x why-2.38/tests/java/Power.java
x why-2.38/tests/java/PreAndOld.java
x why-2.38/tests/java/SimpleApplet.java
x why-2.38/tests/java/MullerTheory.java
x why-2.38/tests/java/MyCosine.java
x why-2.38/tests/java/oracle/
x why-2.38/tests/java/oracle/SimpleAlloc.err.oracle
x why-2.38/tests/java/oracle/Hello.res.oracle
x why-2.38/tests/java/oracle/Counter.err.oracle
x why-2.38/tests/java/oracle/SelectionSort.res.oracle
x why-2.38/tests/java/oracle/Assertion.err.oracle
x why-2.38/tests/java/oracle/SimpleAlloc.res.oracle
x why-2.38/tests/java/oracle/Duplets.err.oracle
x why-2.38/tests/java/oracle/Switch.res.oracle
x why-2.38/tests/java/oracle/TestNonNull.res.oracle
x why-2.38/tests/java/oracle/Bug_sort_exns.res.oracle
x why-2.38/tests/java/oracle/Fresh.res.oracle
x why-2.38/tests/java/oracle/Negate.res.oracle
x why-2.38/tests/java/oracle/Purse.err.oracle
x why-2.38/tests/java/oracle/Bug_sort_exns.err.oracle
x why-2.38/tests/java/oracle/Arrays.res.oracle
x why-2.38/tests/java/oracle/bts15964.err.oracle
x why-2.38/tests/java/oracle/BankingExample.err.oracle
x why-2.38/tests/java/oracle/AllZeros.err.oracle
x why-2.38/tests/java/oracle/Fresh2.res.oracle
x why-2.38/tests/java/oracle/BinarySearchWrong.res.oracle
x why-2.38/tests/java/oracle/Gcd.err.oracle
x why-2.38/tests/java/oracle/bts15964.res.oracle
x why-2.38/tests/java/oracle/ArrayMax.res.oracle
x why-2.38/tests/java/oracle/Counter.res.oracle
x why-2.38/tests/java/oracle/SimpleApplet.res.oracle
x why-2.38/tests/java/oracle/Termination.res.oracle
x why-2.38/tests/java/oracle/TreeMax.res.oracle
x why-2.38/tests/java/oracle/Booleans.res.oracle
x why-2.38/tests/java/oracle/SimpleApplet.err.oracle
x why-2.38/tests/java/oracle/Muller.res.oracle
x why-2.38/tests/java/oracle/Fresh2.err.oracle
x why-2.38/tests/java/oracle/TreeMax.err.oracle
x why-2.38/tests/java/oracle/Power.res.oracle
x why-2.38/tests/java/oracle/Termination.err.oracle
x why-2.38/tests/java/oracle/ArrayMax.err.oracle
x why-2.38/tests/java/oracle/Isqrt.err.oracle
x why-2.38/tests/java/oracle/SideEffects.err.oracle
x why-2.38/tests/java/oracle/Creation.err.oracle
x why-2.38/tests/java/oracle/TestNonNull.err.oracle
x why-2.38/tests/java/oracle/Purse.res.oracle
x why-2.38/tests/java/oracle/MacCarthy.res.oracle
x why-2.38/tests/java/oracle/Sort2.err.oracle
x why-2.38/tests/java/oracle/AllZeros.res.oracle
x why-2.38/tests/java/oracle/BinarySearch.err.oracle
x why-2.38/tests/java/oracle/Fresh3.err.oracle
x why-2.38/tests/java/oracle/FlagStatic.err.oracle
x why-2.38/tests/java/oracle/Sort.res.oracle
x why-2.38/tests/java/oracle/MyCosine.res.oracle
x why-2.38/tests/java/oracle/SelectionSort.err.oracle
x why-2.38/tests/java/oracle/Negate.err.oracle
x why-2.38/tests/java/oracle/Muller.err.oracle
x why-2.38/tests/java/oracle/BankingExample.res.oracle
x why-2.38/tests/java/oracle/Fresh.err.oracle
x why-2.38/tests/java/oracle/Sort.err.oracle
x why-2.38/tests/java/oracle/Booleans.err.oracle
x why-2.38/tests/java/oracle/NameConflicts.res.oracle
x why-2.38/tests/java/oracle/PreAndOld.res.oracle
x why-2.38/tests/java/oracle/NameConflicts.err.oracle
x why-2.38/tests/java/oracle/Fact.res.oracle
x why-2.38/tests/java/oracle/MacCarthy.err.oracle
x why-2.38/tests/java/oracle/MyCosine.err.oracle
x why-2.38/tests/java/oracle/Fact.err.oracle
x why-2.38/tests/java/oracle/MullerTheory.err.oracle
x why-2.38/tests/java/oracle/Switch.err.oracle
x why-2.38/tests/java/oracle/MullerTheory.res.oracle
x why-2.38/tests/java/oracle/Gcd.res.oracle
x why-2.38/tests/java/oracle/Isqrt.res.oracle
x why-2.38/tests/java/oracle/Power.err.oracle
x why-2.38/tests/java/oracle/Literals.res.oracle
x why-2.38/tests/java/oracle/BinarySearchWrong.err.oracle
x why-2.38/tests/java/oracle/PreAndOld.err.oracle
x why-2.38/tests/java/oracle/Hello.err.oracle
x why-2.38/tests/java/oracle/BinarySearch.res.oracle
x why-2.38/tests/java/oracle/Arrays.err.oracle
x why-2.38/tests/java/oracle/Creation.res.oracle
x why-2.38/tests/java/oracle/FlagStatic.res.oracle
x why-2.38/tests/java/oracle/Fresh3.res.oracle
x why-2.38/tests/java/oracle/SideEffects.res.oracle
x why-2.38/tests/java/oracle/Literals.err.oracle
x why-2.38/tests/java/oracle/Fibonacci.res.oracle
x why-2.38/tests/java/oracle/Duplets.res.oracle
x why-2.38/tests/java/oracle/Sort2.res.oracle
x why-2.38/tests/java/oracle/Fibonacci.err.oracle
x why-2.38/tests/java/oracle/Assertion.res.oracle
x why-2.38/tests/java/Gcd.java
x why-2.38/tests/java/SelectionSort.java
x why-2.38/tests/java/Purse.java
x why-2.38/tests/java/Creation.java
x why-2.38/tests/java/Duplets.java
x why-2.38/tests/java/Fresh.java
x why-2.38/tests/java/Muller.java
x why-2.38/tests/java/BankingExample.java
x why-2.38/tests/java/SimpleAlloc.java
x why-2.38/tests/java/Isqrt.java
x why-2.38/tests/java/Hello.java
x why-2.38/tests/java/Switch.java
x why-2.38/tests/java/AllZeros.java
x why-2.38/tests/java/Bug_sort_exns.java
x why-2.38/tests/java/BinarySearch.java
x why-2.38/tests/java/Termination.java
x why-2.38/tests/java/TestNonNull.java
x why-2.38/tests/java/SideEffects.java
x why-2.38/tests/java/Literals.java
x why-2.38/tests/java/Arrays.java
x why-2.38/tests/java/BinarySearchWrong.java
x why-2.38/tests/java/bts15964.java
x why-2.38/tests/java/Assertion.java
x why-2.38/tests/java/Fibonacci.java
x why-2.38/tests/java/TreeMax.java
x why-2.38/tests/java/Sort.java
x why-2.38/tests/java/result/
x why-2.38/tests/java/result/README
x why-2.38/tests/java/Fresh2.java
x why-2.38/tests/java/NameConflicts.java
x why-2.38/tests/java/FlagStatic.java
x why-2.38/tests/java/Sort2.java
x why-2.38/tests/java/Fresh3.java
x why-2.38/tests/java/Counter.java
x why-2.38/tests/java/Negate.java
x why-2.38/tests/java/MacCarthy.java
x why-2.38/tests/java/Fact.java
x why-2.38/tests/java/ArrayMax.java
x why-2.38/tests/c/
x why-2.38/tests/c/muller.c
x why-2.38/tests/c/eps_line1.c
x why-2.38/tests/c/isqrt.c
x why-2.38/tests/c/fact.c
x why-2.38/tests/c/oracle/
x why-2.38/tests/c/oracle/exp.err.oracle
x why-2.38/tests/c/oracle/binary_search_wrong.res.oracle
x why-2.38/tests/c/oracle/power.res.oracle
x why-2.38/tests/c/oracle/minmax.res.oracle
x why-2.38/tests/c/oracle/cd1d.res.oracle
x why-2.38/tests/c/oracle/eps_line2.err.oracle
x why-2.38/tests/c/oracle/scalar_product.res.oracle
x why-2.38/tests/c/oracle/popHeap.err.oracle
x why-2.38/tests/c/oracle/double_rounding_multirounding_model.err.oracle
x why-2.38/tests/c/oracle/sum_array.err.oracle
x why-2.38/tests/c/oracle/isqrt2.err.oracle
x why-2.38/tests/c/oracle/sparse_array2.res.oracle
x why-2.38/tests/c/oracle/sparse_array.res.oracle
x why-2.38/tests/c/oracle/binary_search_wrong.err.oracle
x why-2.38/tests/c/oracle/rec.res.oracle
x why-2.38/tests/c/oracle/eps_line1.res.oracle
x why-2.38/tests/c/oracle/array_double.res.oracle
x why-2.38/tests/c/oracle/conjugate.err.oracle
x why-2.38/tests/c/oracle/array_max.err.oracle
x why-2.38/tests/c/oracle/duplets.err.oracle
x why-2.38/tests/c/oracle/isqrt.res.oracle
x why-2.38/tests/c/oracle/interval_arith.err.oracle
x why-2.38/tests/c/oracle/insertion_sort.err.oracle
x why-2.38/tests/c/oracle/floats_bsearch.err.oracle
x why-2.38/tests/c/oracle/scalar_product.err.oracle
x why-2.38/tests/c/oracle/sum_array.res.oracle
x why-2.38/tests/c/oracle/swap.err.oracle
x why-2.38/tests/c/oracle/Sterbenz.err.oracle
x why-2.38/tests/c/oracle/interval_arith.res.oracle
x why-2.38/tests/c/oracle/insertion_sort.res.oracle
x why-2.38/tests/c/oracle/muller.res.oracle
x why-2.38/tests/c/oracle/duplets.res.oracle
x why-2.38/tests/c/oracle/quick_sort.err.oracle
x why-2.38/tests/c/oracle/sparse_array.err.oracle
x why-2.38/tests/c/oracle/sparse_array2.err.oracle
x why-2.38/tests/c/oracle/array_max.res.oracle
x why-2.38/tests/c/oracle/overflow_level.res.oracle
x why-2.38/tests/c/oracle/floats_bsearch.res.oracle
x why-2.38/tests/c/oracle/cd1d.err.oracle
x why-2.38/tests/c/oracle/find_array.err.oracle
x why-2.38/tests/c/oracle/float_array.err.oracle
x why-2.38/tests/c/oracle/popHeap.res.oracle
x why-2.38/tests/c/oracle/binary_search.res.oracle
x why-2.38/tests/c/oracle/fact.res.oracle
x why-2.38/tests/c/oracle/array_double.err.oracle
x why-2.38/tests/c/oracle/isqrt2.res.oracle
x why-2.38/tests/c/oracle/muller.err.oracle
x why-2.38/tests/c/oracle/maze.err.oracle
x why-2.38/tests/c/oracle/flag.err.oracle
x why-2.38/tests/c/oracle/power.err.oracle
x why-2.38/tests/c/oracle/maze.res.oracle
x why-2.38/tests/c/oracle/double_rounding_strict_model.err.oracle
x why-2.38/tests/c/oracle/clock_drift.res.oracle
x why-2.38/tests/c/oracle/eps_line1.err.oracle
x why-2.38/tests/c/oracle/selection_sort.err.oracle
x why-2.38/tests/c/oracle/tree_max.err.oracle
x why-2.38/tests/c/oracle/selection_sort.res.oracle
x why-2.38/tests/c/oracle/my_cosine.res.oracle
x why-2.38/tests/c/oracle/heap_sort.res.oracle
x why-2.38/tests/c/oracle/my_cosine.err.oracle
x why-2.38/tests/c/oracle/double_rounding_strict_model.res.oracle
x why-2.38/tests/c/oracle/conjugate.res.oracle
x why-2.38/tests/c/oracle/minmax.err.oracle
x why-2.38/tests/c/oracle/binary_heap.res.oracle
x why-2.38/tests/c/oracle/float_sqrt.res.oracle
x why-2.38/tests/c/oracle/binary_heap.err.oracle
x why-2.38/tests/c/oracle/eps_line2.res.oracle
x why-2.38/tests/c/oracle/quick_sort.res.oracle
x why-2.38/tests/c/oracle/find_array.res.oracle
x why-2.38/tests/c/oracle/fact.err.oracle
x why-2.38/tests/c/oracle/fresh.err.oracle
x why-2.38/tests/c/oracle/exp.res.oracle
x why-2.38/tests/c/oracle/fresh.res.oracle
x why-2.38/tests/c/oracle/double_rounding_multirounding_model.res.oracle
x why-2.38/tests/c/oracle/tree_max.res.oracle
x why-2.38/tests/c/oracle/rec.err.oracle
x why-2.38/tests/c/oracle/float_array.res.oracle
x why-2.38/tests/c/oracle/float_sqrt.err.oracle
x why-2.38/tests/c/oracle/isqrt.err.oracle
x why-2.38/tests/c/oracle/flag.res.oracle
x why-2.38/tests/c/oracle/swap.res.oracle
x why-2.38/tests/c/oracle/heap_sort.err.oracle
x why-2.38/tests/c/oracle/Sterbenz.res.oracle
x why-2.38/tests/c/oracle/overflow_level.err.oracle
x why-2.38/tests/c/oracle/clock_drift.err.oracle
x why-2.38/tests/c/oracle/binary_search.err.oracle
x why-2.38/tests/c/maze.c
x why-2.38/tests/c/double_rounding_strict_model.c
x why-2.38/tests/c/array_double.c
x why-2.38/tests/c/interval_arith.c
x why-2.38/tests/c/Sterbenz.jessie/
x why-2.38/tests/c/Sterbenz.jessie/coq/
x why-2.38/tests/c/Sterbenz.jessie/coq/Sterbenz_why.v
x why-2.38/tests/c/reverse_array.c
x why-2.38/tests/c/sum_array.c
x why-2.38/tests/c/insertion_sort.c
x why-2.38/tests/c/find_array.c
x why-2.38/tests/c/duplets.c
x why-2.38/tests/c/quick_sort.c
x why-2.38/tests/c/rec_lin2.c
x why-2.38/tests/c/flag.c
x why-2.38/tests/c/test.c
x why-2.38/tests/c/floats_bsearch.c
x why-2.38/tests/c/array_max.c
x why-2.38/tests/c/tree_max.c
x why-2.38/tests/c/clock_drift.c
x why-2.38/tests/c/float_sqrt.c
x why-2.38/tests/c/popHeap.c
x why-2.38/tests/c/binary_search.c
x why-2.38/tests/c/cd1d.c
x why-2.38/tests/c/sparse_array2.c
x why-2.38/tests/c/heap_sort.c
x why-2.38/tests/c/dirichlet.c
x why-2.38/tests/c/sparse_array.c
x why-2.38/tests/c/my_cosine.c
x why-2.38/tests/c/double_rounding_multirounding_model.c
x why-2.38/tests/c/overflow_level.c
x why-2.38/tests/c/sqrt3.c
x why-2.38/tests/c/selection_sort.c
x why-2.38/tests/c/binary_search_wrong.c
x why-2.38/tests/c/fresh.c
x why-2.38/tests/c/result/
x why-2.38/tests/c/result/README
x why-2.38/tests/c/power.c
x why-2.38/tests/c/scalar_product.c
x why-2.38/tests/c/conjugate.c
x why-2.38/tests/c/my_cosine.jessie/
x why-2.38/tests/c/my_cosine.jessie/coq/
x why-2.38/tests/c/my_cosine.jessie/coq/my_cosine_why.v
x why-2.38/tests/c/exp.c
x why-2.38/tests/c/eps_line2.c
x why-2.38/tests/c/Sterbenz.c
x why-2.38/tests/c/float_array.c
x why-2.38/tests/c/rec.c
x why-2.38/tests/c/isqrt2.c
x why-2.38/tests/c/minmax.c
x why-2.38/tests/c/binary_heap.c
x why-2.38/tests/c/swap.c
x why-2.38/tests/c/triangle.c
x why-2.38/tests/c/sqrt4.c
x why-2.38/Makefile.in
x why-2.38/doc/
x why-2.38/doc/Makefile
x why-2.38/LICENSE
x why-2.38/README
x why-2.38/INSTALL
x why-2.38/Version
x why-2.38/COPYING
x why-2.38/configure.in
x why-2.38/config/
x why-2.38/config/check_ocamlgraph.ml
x why-2.38/version.sh
x why-2.38/.depend
x why-2.38/lib/
x why-2.38/lib/coq-v7/
x why-2.38/lib/coq-v7/WhyBool.v
x why-2.38/lib/coq-v7/WhyTuples.v
x why-2.38/lib/coq-v7/WhyReal.v
x why-2.38/lib/coq-v7/WhyInt.v
x why-2.38/lib/coq-v7/WhyCoq73.v
x why-2.38/lib/coq-v7/WhyCM.v
x why-2.38/lib/coq-v7/WhySorted.v
x why-2.38/lib/coq-v7/WhyTactics.v
x why-2.38/lib/coq-v7/WhyCoqDev.v
x why-2.38/lib/coq-v7/caduceus_why.v
x why-2.38/lib/coq-v7/caduceus_tactics.v
x why-2.38/lib/coq-v7/WhyLemmas.v
x why-2.38/lib/coq-v7/WhyCoqCompat.v
x why-2.38/lib/coq-v7/WhyExn.v
x why-2.38/lib/coq-v7/WhyPermut.v
x why-2.38/lib/coq-v7/WhyArrays.v
x why-2.38/lib/coq-v7/Why.v
x why-2.38/lib/coq/
x why-2.38/lib/coq/WhyBool.v
x why-2.38/lib/coq/WhyTuples.v
x why-2.38/lib/coq/WhyReal.v
x why-2.38/lib/coq/caduceus_lists.v
x why-2.38/lib/coq/JessieGappa.v
x why-2.38/lib/coq/WhyCoq8.v
x why-2.38/lib/coq/WhyInt.v
x why-2.38/lib/coq/WhyArraysFMap.v
x why-2.38/lib/coq/Caduceus.v
x why-2.38/lib/coq/WhyNTMonad.v
x why-2.38/lib/coq/WhyCM.v
x why-2.38/lib/coq/Jessie_memory_model.v
x why-2.38/lib/coq/jessie_why.v
x why-2.38/lib/coq/WhyFloats.v
x why-2.38/lib/coq/WhySorted.v
x why-2.38/lib/coq/WhyTactics.v
x why-2.38/lib/coq/WhyCoqDev.v
x why-2.38/lib/coq/caduceus_why.v
x why-2.38/lib/coq/caduceus_tactics.v
x why-2.38/lib/coq/WhyLemmas.v
x why-2.38/lib/coq/WhyFloatsStrictLegacy.v
x why-2.38/lib/coq/WhyCoqCompat.v
x why-2.38/lib/coq/WhyExn.v
x why-2.38/lib/coq/WhyPermut.v
x why-2.38/lib/coq/WhyArrays.v
x why-2.38/lib/coq/WhyFloatsStrict.v
x why-2.38/lib/coq/WhyPrelude.v
x why-2.38/lib/coq/Why.v
x why-2.38/lib/java_api/
x why-2.38/lib/java_api/java/
x why-2.38/lib/java_api/java/lang/
x why-2.38/lib/java_api/java/lang/Character.java
x why-2.38/lib/java_api/java/lang/Comparable.java
x why-2.38/lib/java_api/java/lang/CharSequence.java
x why-2.38/lib/java_api/java/lang/ArrayStoreException.java
x why-2.38/lib/java_api/java/lang/String.java
x why-2.38/lib/java_api/java/lang/Integer.java
x why-2.38/lib/java_api/java/lang/System.java
x why-2.38/lib/java_api/java/lang/StringBuffer.java
x why-2.38/lib/java_api/java/lang/RuntimeException.java
x why-2.38/lib/java_api/java/lang/Double.java
x why-2.38/lib/java_api/java/lang/Object.java
x why-2.38/lib/java_api/java/lang/NumberFormatException.java
x why-2.38/lib/java_api/java/lang/Class.java
x why-2.38/lib/java_api/java/lang/IllegalArgumentException.java
x why-2.38/lib/java_api/java/lang/Throwable.java
x why-2.38/lib/java_api/java/lang/Long.java
x why-2.38/lib/java_api/java/lang/Math.java
x why-2.38/lib/java_api/java/lang/Cloneable.java
x why-2.38/lib/java_api/java/lang/Number.java
x why-2.38/lib/java_api/java/lang/Exception.java
x why-2.38/lib/java_api/java/util/
x why-2.38/lib/java_api/java/util/HashMapIntegerInteger.java
x why-2.38/lib/java_api/java/util/Set.java
x why-2.38/lib/java_api/java/util/HashMapIntegerLong.java
x why-2.38/lib/java_api/java/util/Collection.java
x why-2.38/lib/java_api/java/util/Iterator.java
x why-2.38/lib/java_api/java/util/HashMap.java
x why-2.38/lib/java_api/java/util/Map.java
x why-2.38/lib/java_api/java/util/Locale.java
x why-2.38/lib/java_api/java/util/AbstractMap.java
x why-2.38/lib/java_api/java/io/
x why-2.38/lib/java_api/java/io/PrintStream.java
x why-2.38/lib/java_api/java/io/FilterOutputStream.java
x why-2.38/lib/java_api/java/io/OutputStreamWriter.java
x why-2.38/lib/java_api/java/io/InputStream.java
x why-2.38/lib/java_api/java/io/File.java
x why-2.38/lib/java_api/java/io/ObjectStreamClass.java
x why-2.38/lib/java_api/java/io/BufferedWriter.java
x why-2.38/lib/java_api/java/io/OutputStream.java
x why-2.38/lib/java_api/java/io/Reader.java
x why-2.38/lib/java_api/java/io/IOException.java
x why-2.38/lib/java_api/java/io/FileReader.java
x why-2.38/lib/java_api/java/io/FileDescriptor.java
x why-2.38/lib/java_api/java/io/Serializable.java
x why-2.38/lib/java_api/java/io/InputStreamReader.java
x why-2.38/lib/java_api/java/io/FileNotFoundException.java
x why-2.38/lib/java_api/java/io/StreamTokenizer.java
x why-2.38/lib/why3/
x why-2.38/lib/why3/jessie_why3integer_obsolete.why
x why-2.38/lib/why3/jessie_why3.mlw
x why-2.38/lib/why3/jessie_why3theories.why
x why-2.38/lib/why3/coq.drv
x why-2.38/lib/pvs/
x why-2.38/lib/pvs/jessie.pvs
x why-2.38/lib/pvs/pvscontext.el
x why-2.38/lib/pvs/whyfloat.prf
x why-2.38/lib/pvs/why.pvs
x why-2.38/lib/pvs/jessie.prf
x why-2.38/lib/pvs/whyfloat.pvs
x why-2.38/lib/pvs/why.prf
x why-2.38/lib/pvs/top.pvs
x why-2.38/lib/isabelle/
x why-2.38/lib/isabelle/caduceus_why.thy
x why-2.38/lib/why/
x why-2.38/lib/why/floats_strict.why
x why-2.38/lib/why/mybag.why
x why-2.38/lib/why/prelude.why
x why-2.38/lib/why/lbmm.why
x why-2.38/lib/why/mix.why
x why-2.38/lib/why/bool.why
x why-2.38/lib/why/caduceus_arith.why
x why-2.38/lib/why/integer.why
x why-2.38/lib/why/bitvector.why
x why-2.38/lib/why/real.why
x why-2.38/lib/why/jessie_bitvectors.why
x why-2.38/lib/why/arrays.why
x why-2.38/lib/why/caduceus.why
x why-2.38/lib/why/floats_multi_rounding.why
x why-2.38/lib/why/divisions.why
x why-2.38/lib/why/floats_full.why
x why-2.38/lib/why/arith.why
x why-2.38/lib/why/jessie.why
x why-2.38/lib/why/caduceus_noalloc.why
x why-2.38/lib/why/floats_common.why
x why-2.38/lib/javacard_api/
x why-2.38/lib/javacard_api/javacard/
x why-2.38/lib/javacard_api/javacard/framework/
x why-2.38/lib/javacard_api/javacard/framework/Shareable.java
x why-2.38/lib/javacard_api/javacard/framework/APDUException.java
x why-2.38/lib/javacard_api/javacard/framework/Dispatcher.java
x why-2.38/lib/javacard_api/javacard/framework/Applet.java
x why-2.38/lib/javacard_api/javacard/framework/Util.java
x why-2.38/lib/javacard_api/javacard/framework/PIN.java
x why-2.38/lib/javacard_api/javacard/framework/ISOException.java
x why-2.38/lib/javacard_api/javacard/framework/PINException.java
x why-2.38/lib/javacard_api/javacard/framework/SystemException.java
x why-2.38/lib/javacard_api/javacard/framework/TransactionException.java
x why-2.38/lib/javacard_api/javacard/framework/JCSystem.java
x why-2.38/lib/javacard_api/javacard/framework/APDU.java
x why-2.38/lib/javacard_api/javacard/framework/CardException.java
x why-2.38/lib/javacard_api/javacard/framework/AID.java
x why-2.38/lib/javacard_api/javacard/framework/CardRuntimeException.java
x why-2.38/lib/javacard_api/javacard/framework/OwnerPIN.java
x why-2.38/lib/javacard_api/javacard/framework/ISO7816.java
x why-2.38/lib/javacard_api/javacard/framework/UserException.java
x why-2.38/lib/javacard_api/javacard/security/
x why-2.38/lib/javacard_api/javacard/security/RandomData.java
x why-2.38/lib/javacard_api/javacard/security/RSAPublicKey.java
x why-2.38/lib/javacard_api/javacard/security/CryptoException.java
x why-2.38/lib/javacard_api/javacard/security/PublicKey.java
x why-2.38/lib/javacard_api/javacard/security/Key.java
x why-2.38/lib/javacard_api/javacard/security/DSAKey.java
x why-2.38/lib/javacard_api/javacard/security/DSAPrivateKey.java
x why-2.38/lib/javacard_api/javacard/security/DSAPublicKey.java
x why-2.38/lib/javacard_api/javacard/security/RSAPrivateCrtKey.java
x why-2.38/lib/javacard_api/javacard/security/KeyBuilder.java
x why-2.38/lib/javacard_api/javacard/security/Signature.java
x why-2.38/lib/javacard_api/javacard/security/PrivateKey.java
x why-2.38/lib/javacard_api/javacard/security/KeyPair.java
x why-2.38/lib/javacard_api/javacard/security/SecretKey.java
x why-2.38/lib/javacard_api/javacard/security/DESKey.java
x why-2.38/lib/javacard_api/javacard/security/MessageDigest.java
x why-2.38/lib/javacard_api/javacard/security/RSAPrivateKey.java
x why-2.38/lib/javacard_api/java/
x why-2.38/lib/javacard_api/java/lang/
x why-2.38/lib/javacard_api/java/lang/RuntimeException.java
x why-2.38/lib/javacard_api/java/lang/IndexOutOfBoundsException.java
x why-2.38/lib/javacard_api/java/lang/Object.java
x why-2.38/lib/javacard_api/java/lang/Throwable.java
x why-2.38/lib/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java
x why-2.38/lib/javacard_api/java/lang/Exception.java
x why-2.38/lib/javacard_api/com/
x why-2.38/lib/javacard_api/com/sun/
x why-2.38/lib/javacard_api/com/sun/javacard/
x why-2.38/lib/javacard_api/com/sun/javacard/impl/
x why-2.38/lib/javacard_api/com/sun/javacard/impl/NativeMethods.java
x why-2.38/lib/javacard_api/com/sun/javacard/impl/PackedBoolean.java
x why-2.38/lib/javacard_api/com/sun/javacard/impl/PrivAccess.java
x why-2.38/lib/javacard_api/com/sun/javacard/impl/Constants.java
x why-2.38/lib/javacard_api/javacardx/
x why-2.38/lib/javacard_api/javacardx/crypto/
x why-2.38/lib/javacard_api/javacardx/crypto/Cipher.java
x why-2.38/.depend.coq
x why-2.38/CHANGES
x why-2.38/atp/
x why-2.38/atp/fourier_motzkin.ml
x why-2.38/atp/LICENSE.txt
x why-2.38/atp/cooper.ml
x why-2.38/atp/qelim.ml
x why-2.38/atp/Quotexpander.ml
x why-2.38/atp/fol.ml
x why-2.38/atp/dp.ml
x why-2.38/atp/Mk_ml_file
x why-2.38/atp/make.ml
x why-2.38/atp/skolem.ml
x why-2.38/atp/intro.ml
x why-2.38/atp/lib.ml
x why-2.38/atp/defcnf.ml
x why-2.38/atp/herbrand.ml
x why-2.38/atp/propexamples.ml
x why-2.38/atp/prop.ml
x why-2.38/atp/formulas.ml
x why-2.38/atp/Makefile
x why-2.38/configure
x why-2.38/bin/
x why-2.38/src/
x why-2.38/src/red.mli
x why-2.38/src/predDefExpansor.mli
x why-2.38/src/cvcl.ml
x why-2.38/src/annot.mli
x why-2.38/src/zenon.mli
x why-2.38/src/ident.mli
x why-2.38/src/logic.mli
x why-2.38/src/unionfind.ml
x why-2.38/src/why3.ml
x why-2.38/src/why3.mli
x why-2.38/src/wp.ml
x why-2.38/src/cvcl.mli
x why-2.38/src/ocaml.ml
x why-2.38/src/annot.ml
x why-2.38/src/parser.mly
x why-2.38/src/simplify.ml
x why-2.38/src/z3.ml
x why-2.38/src/monad.mli
x why-2.38/src/encoding.ml
x why-2.38/src/misc.mli
x why-2.38/src/option_misc.mli
x why-2.38/src/pp.mli
x why-2.38/src/monad.ml
x why-2.38/src/hol4.mli
x why-2.38/src/mizar.mli
x why-2.38/src/encoding_mono_inst.mli
x why-2.38/src/wserver.mli
x why-2.38/src/rc.mll
x why-2.38/src/main.ml
x why-2.38/src/option_misc.ml
x why-2.38/src/encoding_rec.mli
x why-2.38/src/wserver.ml
x why-2.38/src/predDefExpansor.ml
x why-2.38/src/purify.mli
x why-2.38/src/parser.mli
x why-2.38/src/simplify.mli
x why-2.38/src/encoding_mono_inst.ml
x why-2.38/src/dispatcher.mli
x why-2.38/src/fpi.ml
x why-2.38/src/coq.ml
x why-2.38/src/types.mli
x why-2.38/src/pvs.ml
x why-2.38/src/encoding_strat.ml
x why-2.38/src/ocaml.mli
x why-2.38/src/loc.ml
x why-2.38/src/why3_kw.mli
x why-2.38/src/red.ml
x why-2.38/src/encoding_pred.mli
x why-2.38/src/pvs.mli
x why-2.38/src/rename.mli
x why-2.38/src/env.ml
x why-2.38/src/env.mli
x why-2.38/src/ltyping.ml
x why-2.38/src/monomorph.ml
x why-2.38/src/explain.mli
x why-2.38/src/why3_kw.ml
x why-2.38/src/options.ml
x why-2.38/src/effect.mli
x why-2.38/src/misc.ml
x why-2.38/src/graphviz.ml
x why-2.38/src/typing.mli
x why-2.38/src/isabelle.mli
x why-2.38/src/pretty.mli
x why-2.38/src/wserver.ml4
x why-2.38/src/monomorph.mli
x why-2.38/src/xml.mll
x why-2.38/src/fpi.mli
x why-2.38/src/explain.ml
x why-2.38/src/mlize.mli
x why-2.38/src/hypotheses_filtering.ml
x why-2.38/src/lib.ml
x why-2.38/src/options.mli
x why-2.38/src/linenum.mll
x why-2.38/src/whyweb.ml
x why-2.38/src/encoding_strat.mli
x why-2.38/src/dispatcher.ml
x why-2.38/src/linenum.mli
x why-2.38/src/parser.ml
x why-2.38/src/effect.ml
x why-2.38/src/ltyping.mli
x why-2.38/src/encoding_pred.ml
x why-2.38/src/report.ml
x why-2.38/src/rename.ml
x why-2.38/src/smtlib.mli
x why-2.38/src/print_real.ml
x why-2.38/src/gappa.ml
x why-2.38/src/smtlib.ml
x why-2.38/src/zenon.ml
x why-2.38/src/vcg.mli
x why-2.38/src/mapenv.ml
x why-2.38/src/encoding_rec.ml
x why-2.38/src/xml.mli
x why-2.38/src/fastwp.mli
x why-2.38/src/typing.ml
x why-2.38/src/mlize.ml
x why-2.38/src/wp.mli
x why-2.38/src/log.mli
x why-2.38/src/linenum.ml
x why-2.38/src/version.ml
x why-2.38/src/gappa.mli
x why-2.38/src/ident.ml
x why-2.38/src/ptree.mli
x why-2.38/src/util.ml
x why-2.38/src/regen.ml
x why-2.38/src/project.ml
x why-2.38/src/error.mli
x why-2.38/src/why.ml
x why-2.38/src/fastwp.ml
x why-2.38/src/lib.mli
x why-2.38/src/harvey.mli
x why-2.38/src/graphviz.mli
x why-2.38/src/regen.mli
x why-2.38/src/lexer.mll
x why-2.38/src/rc.mli
x why-2.38/src/vcg.ml
x why-2.38/src/logic_decl.mli
x why-2.38/src/project.mli
x why-2.38/src/pretty.ml
x why-2.38/src/cc.mli
x why-2.38/src/theoryreducer.ml
x why-2.38/src/encoding_mono2.ml
x why-2.38/src/coq.mli
x why-2.38/src/harvey.ml
x why-2.38/src/mizar.ml
x why-2.38/src/lexer.mli
x why-2.38/src/monadSig.mli
x why-2.38/src/z3.mli
x why-2.38/src/encoding_mono.ml
x why-2.38/src/encoding.mli
x why-2.38/src/util.mli
x why-2.38/src/pp.ml
x why-2.38/src/loc.mli
x why-2.38/src/holl.ml
x why-2.38/src/isabelle.ml
x why-2.38/src/holl.mli
x why-2.38/src/theory_filtering.ml
x why-2.38/src/lexer.ml
x why-2.38/src/ast.mli
x why-2.38/src/report.mli
x why-2.38/src/hol4.ml
checking for ocamlc... ocamlc
ocaml version is 4.03.0
ocaml library path is /Users/david/.opam/4.03.0/lib/ocaml
checking for ocamlfind... yes
checking OS dependent settings... Unix
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version... ok
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
ocamlfind found ocamlgraph in /Users/david/.opam/4.03.0/lib/ocamlgraph
checking for ocamlweb... true
checking for frama-c... /Users/david/.opam/4.03.0/bin/frama-c
checking Frama-c version...
configure: WARNING: bad Frama-c version "", you need version Silicon
checking for why3... /Users/david/.opam/4.03.0/bin/why3
checking Why3 version...
configure: WARNING: unknown version , hope this works
checking for coqc... no
configure: WARNING: Cannot find coqc.
checking for pvs... no
configure: WARNING: Cannot find PVS.
configure: creating ./config.status
config.status: creating Makefile

                 Summary
-----------------------------------------
OCaml version            : 4.03.0
OCaml library path       : /Users/david/.opam/4.03.0/lib/ocaml
OcamlGraph lib           : found by ocamlfind
Verbose make             : no
Inference of annotations : no
Why3 support             : yes
    Binary               : /Users/david/.opam/4.03.0/bin/why3
    Version              :
    unknown version , hope this works
Frama-C plugin           : no
Coq support (via Why3)   : no
    command 'coqc' not found
PVS support (via Why3)   : no
    command 'pvs' not found
Other provers support    : (via Why3)

Thanks,
Junkil

> On Aug 22, 2017, at 4:41 AM, Claude Marché <Claude.Marche at inria.fr> wrote:
> 
> 
> 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                    |
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss