This is an automated email from the git hooks/post-receive script. treinen pushed a change to branch master in repository why.
from 11cf726 set FRAMADIR
adds e2becea Imported Upstream version 2.35
adds 460c3c0 New upstream version 2.36
new 464673e New upstream version 2.38
new e3b175d Updated version 2.38 from 'upstream/2.38'
new 01c83ee new upstream
new 9314605 adapt patches to new upstream
new c3465b1 bump build-dependency on frama-c to Silicon
new a60197e install Jessie.o
new f3cc2fb close bug 858366
new f8538ba restrict to native architectures
The 8 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
.depend | 1064 ++++++++++++-------------
.depend.coq | 99 ++-
CHANGES | 13 +
Makefile.in | 547 +------------
README | 3 +-
Version | 2 +-
atp/Quotexpander.ml | 3 +-
atp/cooper.ml | 3 +-
atp/defcnf.ml | 3 +-
atp/dp.ml | 3 +-
atp/fol.ml | 3 +-
atp/formulas.ml | 3 +-
atp/fourier_motzkin.ml | 3 +-
atp/herbrand.ml | 3 +-
atp/intro.ml | 3 +-
atp/lib.ml | 3 +-
atp/make.ml | 3 +-
atp/prop.ml | 3 +-
atp/propexamples.ml | 3 +-
atp/qelim.ml | 3 +-
atp/skolem.ml | 3 +-
config/check_ocamlgraph.ml | 3 +-
configure | 43 +-
configure.in | 131 +--
debian/changelog | 14 +
debian/control | 4 +-
debian/patches/bprintf | 6 +-
debian/patches/edge | 6 +-
debian/patches/reproducible_build | 48 +-
debian/why.install | 1 +
frama-c-plugin/Jessie.mli | 3 +-
frama-c-plugin/Makefile | 4 +-
frama-c-plugin/common.ml | 25 +-
frama-c-plugin/common.mli | 9 +-
frama-c-plugin/interp.ml | 96 +--
frama-c-plugin/interp.mli | 3 +-
frama-c-plugin/jessie_config.ml | 30 +
frama-c-plugin/jessie_integer.ml | 3 +-
frama-c-plugin/jessie_options.ml | 3 +-
frama-c-plugin/jessie_options.mli | 3 +-
frama-c-plugin/norm.ml | 14 +-
frama-c-plugin/norm.mli | 3 +-
frama-c-plugin/register.ml | 3 +-
frama-c-plugin/retype.ml | 3 +-
frama-c-plugin/rewrite.ml | 35 +-
java/java_abstract.ml | 3 +-
java/java_analysis.ml | 3 +-
java/java_ast.mli | 3 +-
java/java_callgraph.ml | 3 +-
java/java_callgraph.mli | 3 +-
java/java_env.mli | 3 +-
java/java_interp.ml | 3 +-
java/java_lexer.mll | 3 +-
java/java_main.ml | 3 +-
java/java_options.ml | 8 +-
java/java_parser.mly | 3 +-
java/java_pervasives.ml | 3 +-
java/java_syntax.ml | 3 +-
java/java_tast.mli | 3 +-
java/java_typing.ml | 3 +-
java/java_typing.mli | 3 +-
jc/jc_ai.mli | 3 +-
jc/jc_annot_fail.ml | 3 +-
jc/jc_annot_inference.ml | 3 +-
jc/jc_ast.mli | 3 +-
jc/jc_callgraph.ml | 3 +-
jc/jc_callgraph.mli | 3 +-
jc/jc_common_options.ml | 3 +-
jc/jc_common_options.mli | 3 +-
jc/jc_constructors.ml | 3 +-
jc/jc_constructors.mli | 3 +-
jc/jc_control_flow.ml | 3 +-
jc/jc_effect.ml | 3 +-
jc/jc_env.mli | 3 +-
jc/jc_envset.ml | 3 +-
jc/jc_envset.mli | 3 +-
jc/jc_fenv.ml | 3 +-
jc/jc_frame.ml | 3 +-
jc/jc_frame.mli | 3 +-
jc/jc_frame_notin.ml | 3 +-
jc/jc_interp.ml | 3 +-
jc/jc_interp.mli | 3 +-
jc/jc_interp_misc.ml | 3 +-
jc/jc_interp_misc.mli | 3 +-
jc/jc_invariants.ml | 3 +-
jc/jc_iterators.ml | 3 +-
jc/jc_iterators.mli | 3 +-
jc/jc_lexer.mli | 3 +-
jc/jc_lexer.mll | 3 +-
jc/jc_main.ml | 3 +-
jc/jc_make.ml | 3 +-
jc/jc_name.ml | 3 +-
jc/jc_norm.ml | 3 +-
jc/jc_norm.mli | 3 +-
jc/jc_noutput.ml | 3 +-
jc/jc_options.ml | 8 +-
jc/jc_options.mli | 3 +-
jc/jc_output.ml | 3 +-
jc/jc_output_misc.ml | 3 +-
jc/jc_parser.mly | 3 +-
jc/jc_pattern.ml | 3 +-
jc/jc_pervasives.ml | 3 +-
jc/jc_pervasives.mli | 3 +-
jc/jc_poutput.ml | 3 +-
jc/jc_region.ml | 3 +-
jc/jc_separation.ml | 3 +-
jc/jc_stdlib_ge312.ml | 3 +-
jc/jc_stdlib_ge400.ml | 3 +-
jc/jc_stdlib_lt312.ml | 3 +-
jc/jc_struct_tools.ml | 3 +-
jc/jc_struct_tools.mli | 3 +-
jc/jc_type_var.ml | 3 +-
jc/jc_type_var.mli | 3 +-
jc/jc_typing.ml | 3 +-
jc/jc_typing.mli | 3 +-
jc/numconst.mli | 3 +-
jc/numconst.mll | 3 +-
jc/output.ml | 3 +-
jc/output.mli | 3 +-
mix/mix_ast.mli | 3 +-
mix/mix_cfg.ml | 3 +-
mix/mix_cfg.mli | 3 +-
mix/mix_interp.ml | 3 +-
mix/mix_lexer.mll | 3 +-
mix/mix_main.ml | 3 +-
mix/mix_parser.mly | 3 +-
mix/mix_seq.ml | 3 +-
mix/test.ml | 3 +-
src/annot.ml | 3 +-
src/annot.mli | 3 +-
src/ast.mli | 3 +-
src/cc.mli | 3 +-
src/coq.ml | 3 +-
src/coq.mli | 3 +-
src/cvcl.ml | 3 +-
src/cvcl.mli | 3 +-
src/dispatcher.ml | 3 +-
src/dispatcher.mli | 3 +-
src/effect.ml | 3 +-
src/effect.mli | 3 +-
src/encoding.ml | 3 +-
src/encoding.mli | 3 +-
src/encoding_mono.ml | 3 +-
src/encoding_mono2.ml | 3 +-
src/encoding_mono_inst.ml | 3 +-
src/encoding_mono_inst.mli | 3 +-
src/encoding_pred.ml | 3 +-
src/encoding_pred.mli | 3 +-
src/encoding_rec.ml | 3 +-
src/encoding_rec.mli | 3 +-
src/encoding_strat.ml | 3 +-
src/encoding_strat.mli | 3 +-
src/env.ml | 3 +-
src/env.mli | 3 +-
src/error.mli | 3 +-
src/explain.ml | 3 +-
src/explain.mli | 3 +-
src/fastwp.ml | 3 +-
src/fastwp.mli | 3 +-
src/fpi.ml | 3 +-
src/fpi.mli | 3 +-
src/gappa.ml | 3 +-
src/gappa.mli | 3 +-
src/graphviz.ml | 3 +-
src/graphviz.mli | 3 +-
src/harvey.ml | 3 +-
src/harvey.mli | 3 +-
src/hol4.ml | 3 +-
src/hol4.mli | 3 +-
src/holl.ml | 3 +-
src/holl.mli | 3 +-
src/hypotheses_filtering.ml | 3 +-
src/ident.ml | 3 +-
src/ident.mli | 3 +-
src/isabelle.ml | 3 +-
src/isabelle.mli | 3 +-
src/lexer.ml | 175 ++--
src/lexer.mli | 3 +-
src/lexer.mll | 3 +-
src/lib.ml | 3 +-
src/lib.mli | 3 +-
src/linenum.ml | 21 +-
src/linenum.mli | 3 +-
src/linenum.mll | 3 +-
src/loc.ml | 3 +-
src/loc.mli | 3 +-
src/log.mli | 3 +-
src/logic.mli | 3 +-
src/logic_decl.mli | 3 +-
src/ltyping.ml | 3 +-
src/ltyping.mli | 3 +-
src/main.ml | 3 +-
src/mapenv.ml | 3 +-
src/misc.ml | 3 +-
src/misc.mli | 3 +-
src/mizar.ml | 3 +-
src/mizar.mli | 3 +-
src/mlize.ml | 3 +-
src/mlize.mli | 3 +-
src/monad.ml | 3 +-
src/monad.mli | 3 +-
src/monadSig.mli | 3 +-
src/monomorph.ml | 3 +-
src/monomorph.mli | 3 +-
src/ocaml.ml | 3 +-
src/ocaml.mli | 3 +-
src/option_misc.ml | 3 +-
src/option_misc.mli | 3 +-
src/options.ml | 3 +-
src/options.mli | 3 +-
src/parser.ml | 456 +++++------
src/parser.mly | 3 +-
src/pp.ml | 3 +-
src/pp.mli | 3 +-
src/predDefExpansor.ml | 3 +-
src/predDefExpansor.mli | 3 +-
src/pretty.ml | 3 +-
src/pretty.mli | 3 +-
src/print_real.ml | 3 +-
src/project.ml | 3 +-
src/project.mli | 3 +-
src/ptree.mli | 3 +-
src/purify.mli | 3 +-
src/pvs.ml | 3 +-
src/pvs.mli | 3 +-
src/rc.ml | 820 -------------------
src/rc.mli | 3 +-
src/rc.mll | 3 +-
src/red.ml | 3 +-
src/red.mli | 3 +-
src/regen.ml | 3 +-
src/regen.mli | 3 +-
src/rename.ml | 3 +-
src/rename.mli | 3 +-
src/report.ml | 22 +-
src/report.mli | 3 +-
src/simplify.ml | 3 +-
src/simplify.mli | 3 +-
src/smtlib.ml | 3 +-
src/smtlib.mli | 3 +-
src/theory_filtering.ml | 3 +-
src/theoryreducer.ml | 3 +-
src/types.mli | 3 +-
src/typing.ml | 3 +-
src/typing.mli | 3 +-
src/unionfind.ml | 3 +-
src/util.ml | 3 +-
src/util.mli | 3 +-
src/vcg.ml | 3 +-
src/vcg.mli | 3 +-
src/version.ml | 4 +-
src/why.ml | 3 +-
src/why3.ml | 3 +-
src/why3.mli | 3 +-
src/why3_kw.ml | 3 +-
src/why3_kw.mli | 3 +-
src/whyweb.ml | 3 +-
src/wp.ml | 3 +-
src/wp.mli | 3 +-
src/wserver.ml | 3 +-
src/wserver.ml4 | 3 +-
src/wserver.mli | 3 +-
src/xml.ml | 955 ----------------------
src/xml.mli | 3 +-
src/xml.mll | 3 +-
src/z3.ml | 3 +-
src/z3.mli | 3 +-
src/zenon.ml | 3 +-
src/zenon.mli | 3 +-
tests/c/Sterbenz.c | 3 +-
tests/c/array_double.c | 3 +-
tests/c/array_max.c | 3 +-
tests/c/binary_heap.c | 3 +-
tests/c/binary_search.c | 3 +-
tests/c/binary_search_wrong.c | 3 +-
tests/c/cd1d.c | 3 +-
tests/c/clock_drift.c | 3 +-
tests/c/conjugate.c | 3 +-
tests/c/dirichlet.c | 166 ++++
tests/c/double_rounding_multirounding_model.c | 3 +-
tests/c/double_rounding_strict_model.c | 3 +-
tests/c/duplets.c | 3 +-
tests/c/eps_line1.c | 3 +-
tests/c/eps_line2.c | 3 +-
tests/c/exp.c | 3 +-
tests/c/fact.c | 29 +
tests/c/find_array.c | 3 +-
tests/c/flag.c | 3 +-
tests/c/float_array.c | 3 +-
tests/c/float_sqrt.c | 3 +-
tests/c/floats_bsearch.c | 3 +-
tests/c/fresh.c | 29 +
tests/c/heap_sort.c | 3 +-
tests/c/insertion_sort.c | 3 +-
tests/c/interval_arith.c | 3 +-
tests/c/isqrt.c | 3 +-
tests/c/isqrt2.c | 3 +-
tests/c/maze.c | 3 +-
tests/c/minmax.c | 3 +-
tests/c/muller.c | 3 +-
tests/c/my_cosine.c | 3 +-
tests/c/overflow_level.c | 3 +-
tests/c/popHeap.c | 3 +-
tests/c/power.c | 3 +-
tests/c/quick_sort.c | 3 +-
tests/c/rec.c | 3 +-
tests/c/{rec.c => rec_lin2.c} | 70 +-
tests/c/reverse_array.c | 29 +
tests/c/scalar_product.c | 3 +-
tests/c/selection_sort.c | 3 +-
tests/c/sparse_array.c | 3 +-
tests/c/sparse_array2.c | 3 +-
tests/c/sqrt3.c | 112 +++
tests/c/sqrt4.c | 75 ++
tests/c/sum_array.c | 3 +-
tests/c/swap.c | 3 +-
tests/{java/bts15964.java => c/test.c} | 11 +-
tests/c/tree_max.c | 3 +-
tests/c/triangle.c | 30 +
tests/java/AllZeros.java | 3 +-
tests/java/ArrayMax.java | 3 +-
tests/java/Arrays.java | 3 +-
tests/java/Assertion.java | 3 +-
tests/java/BankingExample.java | 30 +
tests/java/BinarySearch.java | 3 +-
tests/java/BinarySearchWrong.java | 3 +-
tests/java/Bug_sort_exns.java | 3 +-
tests/java/Counter.java | 3 +-
tests/java/Creation.java | 3 +-
tests/java/Duplets.java | 3 +-
tests/java/Fact.java | 3 +-
tests/java/Fibonacci.java | 3 +-
tests/java/FlagStatic.java | 3 +-
tests/java/Fresh.java | 3 +-
tests/java/Fresh2.java | 3 +-
tests/java/Fresh3.java | 3 +-
tests/java/Gcd.java | 3 +-
tests/java/Hello.java | 3 +-
tests/java/Isqrt.java | 3 +-
tests/java/Literals.java | 3 +-
tests/java/MacCarthy.java | 3 +-
tests/java/Muller.java | 3 +-
tests/java/MullerTheory.java | 3 +-
tests/java/MyCosine.java | 3 +-
tests/java/NameConflicts.java | 3 +-
tests/java/Negate.java | 3 +-
tests/java/Power.java | 3 +-
tests/java/PreAndOld.java | 3 +-
tests/java/Purse.java | 3 +-
tests/java/SelectionSort.java | 3 +-
tests/java/SideEffects.java | 3 +-
tests/java/SimpleAlloc.java | 3 +-
tests/java/SimpleApplet.java | 3 +-
tests/java/Sort.java | 3 +-
tests/java/Sort2.java | 3 +-
tests/java/Switch.java | 3 +-
tests/java/Termination.java | 3 +-
tests/java/TestNonNull.java | 3 +-
tests/java/TreeMax.java | 3 +-
tests/java/bts15964.java | 3 +-
tools/regtest.ml | 3 +-
version.sh | 14 +-
362 files changed, 2009 insertions(+), 4212 deletions(-)
create mode 100644 debian/why.install
delete mode 100644 src/rc.ml
delete mode 100644 src/xml.ml
create mode 100644 tests/c/dirichlet.c
copy tests/c/{rec.c => rec_lin2.c} (70%)
create mode 100644 tests/c/sqrt3.c
create mode 100644 tests/c/sqrt4.c
copy tests/{java/bts15964.java => c/test.c} (90%)
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
