[Pkg-ocaml-maint-commits] [why] 01/10: Merge tag 'upstream/2.35'
Ralf Treinen
treinen at moszumanska.debian.org
Tue Oct 11 19:45:10 UTC 2016
This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch try
in repository why.
commit 8c0349f3018140d9f6e503cda5df56586ea008df
Merge: e74847a e2becea
Author: Ralf Treinen <treinen at free.fr>
Date: Tue Mar 15 20:52:33 2016 +0100
Merge tag 'upstream/2.35'
Upstream version 2.35
.depend | 580 ++--
CHANGES | 13 +-
Makefile.in | 71 +-
Version | 6 +-
configure | 334 +-
configure.in | 216 +-
doc/Makefile | 4 +-
frama-c-plugin/Makefile | 11 +-
frama-c-plugin/common.ml | 19 +-
frama-c-plugin/common.mli | 6 +
frama-c-plugin/interp.ml | 14 +
frama-c-plugin/jessie_config.ml | 31 -
frama-c-plugin/jessie_options.ml | 12 +-
frama-c-plugin/ptests_local_config.ml | 37 -
frama-c-plugin/register.ml | 2 +-
frama-c-plugin/rewrite.ml | 39 +-
intf/astnprinter.ml | 1 -
intf/astpprinter.ml | 1 -
intf/astprinter.ml | 4 +-
intf/cache.ml | 2 -
intf/model.ml | 8 +-
intf/pprinter.ml | 205 +-
intf/stat.ml | 5 -
intf/tagsplit.mll | 2 -
java/java_abstract.ml | 2 +-
java/java_analysis.ml | 2 +-
java/java_interp.ml | 5 +-
java/java_main.ml | 1 -
java/java_options.ml | 6 +-
java/java_parser.mly | 1 -
java/java_typing.ml | 11 +-
jc/jc_ai.mli | 1 -
jc/jc_annot_fail.ml | 2 +
jc/jc_ast.mli | 2 -
jc/jc_callgraph.ml | 3 +-
jc/jc_constructors.ml | 29 +-
jc/jc_effect.ml | 2 +-
jc/jc_envset.ml | 2 +
jc/jc_frame.ml | 666 ++--
jc/jc_frame_notin.ml | 6 -
jc/jc_interp.ml | 8 +-
jc/jc_interp_misc.ml | 22 +-
jc/jc_invariants.ml | 2 +-
jc/jc_iterators.ml | 10 +-
jc/jc_iterators.mli | 2 +
jc/jc_lexer.mll | 4 +
jc/jc_main.ml | 1 -
jc/jc_make.ml | 4 +-
jc/jc_name.ml | 3 +-
jc/jc_norm.ml | 7 +-
jc/jc_norm.mli | 2 -
jc/jc_options.ml | 8 +-
jc/jc_parser.mly | 2 -
jc/jc_pervasives.ml | 19 +-
jc/jc_pervasives.mli | 2 +
jc/jc_poutput.ml | 3 -
jc/jc_region.ml | 134 +-
jc/jc_separation.ml | 1 -
jc/jc_stdlib_ge40.ml | 260 --
jc/jc_typing.ml | 10 +-
jc/output.ml | 35 +-
lib/coq/WhyFloats.v | 7 +-
lib/why3/coq.drv | 4 +-
lib/why3/{jessie3.mlw => jessie_why3.mlw} | 2 +-
...integer.why => jessie_why3integer_obsolete.why} | 2 +
...jessie3theories.why => jessie_why3theories.why} | 0
src/coq.ml | 6 +-
src/coq.mli | 6 -
src/cvcl.ml | 26 +-
src/cvcl.mli | 7 -
src/dispatcher.ml | 3 +-
src/effect.ml | 4 +
src/encoding.mli | 2 -
src/encoding_mono.ml | 2 +-
src/encoding_mono_inst.ml | 280 +-
src/encoding_pred.ml | 78 +-
src/encoding_pred.mli | 5 -
src/encoding_rec.ml | 124 +-
src/encoding_rec.mli | 5 -
src/encoding_strat.ml | 88 +-
src/encoding_strat.mli | 5 -
src/env.ml | 6 +
src/explain.ml | 3 +-
src/fastwp.ml | 8 +-
src/gappa.ml | 9 +-
src/gappa.mli | 7 -
src/harvey.ml | 1 -
src/harvey.mli | 7 -
src/hol4.ml | 4 +-
src/hol4.mli | 7 -
src/holl.ml | 2 -
src/holl.mli | 7 -
src/hypotheses_filtering.ml | 6 -
src/isabelle.ml | 8 +-
src/isabelle.mli | 4 -
src/loc.ml | 2 +
src/misc.ml | 157 +-
src/misc.mli | 1 -
src/mizar.ml | 38 +-
src/mizar.mli | 6 -
src/mlize.mli | 2 -
src/monad.ml | 5 +-
src/monomorph.ml | 9 +-
src/ocaml.ml | 2 +
src/options.ml | 334 +-
src/parser.mly | 3 +-
src/predDefExpansor.ml | 3 +-
src/pretty.ml | 2 +
src/project.ml | 3 +-
src/pvs.ml | 5 +-
src/pvs.mli | 7 -
src/red.ml | 4 +-
src/regen.ml | 2 -
src/regen.mli | 1 -
src/rename.ml | 4 +-
src/report.ml | 7 +-
src/simplify.ml | 129 +-
src/simplify.mli | 6 -
src/smtlib.ml | 20 +-
src/smtlib.mli | 6 -
src/theory_filtering.ml | 9 +-
src/theoryreducer.ml | 8 -
src/typing.ml | 17 +-
src/util.ml | 24 +-
src/util.mli | 1 -
src/vcg.ml | 18 +-
src/vcg.mli | 1 -
src/why3.ml | 3 +-
src/wp.ml | 7 +
src/z3.ml | 8 +-
src/z3.mli | 6 -
src/zenon.ml | 118 +-
src/zenon.mli | 7 -
tests/c/Sterbenz.jessie/coq/floats_strict_why.v | 289 --
tests/c/array_max.c | 2 +-
tests/c/binary_search.c | 2 +-
tests/c/{binary_search.c => binary_search_wrong.c} | 2 +-
tests/c/duplets.c | 6 +-
tests/c/float_array.c | 12 +-
tests/c/fresh.c | 33 +
tests/c/my_cosine.c | 2 +-
tests/c/oracle/Sterbenz.res.oracle | 28 +-
tests/c/oracle/array_double.res.oracle | 188 +-
tests/c/oracle/array_max.res.oracle | 192 +-
tests/c/oracle/binary_heap.res.oracle | 26 +-
tests/c/oracle/binary_search.res.oracle | 26 +-
tests/c/oracle/cd1d.res.oracle | 115 +-
tests/c/oracle/clock_drift.res.oracle | 28 +-
tests/c/oracle/conjugate.res.oracle | 241 +-
.../double_rounding_multirounding_model.res.oracle | 68 +-
.../oracle/double_rounding_strict_model.res.oracle | 68 +-
tests/c/oracle/duplets.res.oracle | 599 ++--
tests/c/oracle/eps_line1.res.oracle | 232 +-
tests/c/oracle/eps_line2.res.oracle | 232 +-
tests/c/oracle/exp.res.oracle | 93 +-
tests/c/oracle/find_array.res.oracle | 197 +-
tests/c/oracle/flag.res.oracle | 26 +-
tests/c/oracle/float_array.res.oracle | 665 ++--
tests/c/oracle/float_sqrt.res.oracle | 26 +-
tests/c/oracle/floats_bsearch.res.oracle | 26 +-
tests/c/oracle/heap_sort.res.oracle | 26 +-
tests/c/oracle/insertion_sort.res.oracle | 26 +-
tests/c/oracle/interval_arith.res.oracle | 627 ++--
tests/c/oracle/isqrt.res.oracle | 26 +-
tests/c/oracle/isqrt2.res.oracle | 3545 +++++++++++++++++++-
tests/c/oracle/maze.res.oracle | 22 +-
tests/c/oracle/minmax.res.oracle | 26 +-
tests/c/oracle/muller.res.oracle | 26 +-
tests/c/oracle/my_cosine.res.oracle | 52 +-
tests/c/oracle/overflow_level.res.oracle | 79 +-
tests/c/oracle/popHeap.res.oracle | 555 +--
tests/c/oracle/power.res.oracle | 169 +-
tests/c/oracle/quick_sort.res.oracle | 26 +-
tests/c/oracle/rec.res.oracle | 26 +-
tests/c/oracle/scalar_product.res.oracle | 222 +-
tests/c/oracle/selection_sort.res.oracle | 26 +-
tests/c/oracle/sparse_array.res.oracle | 22 +-
tests/c/oracle/sparse_array2.res.oracle | 26 +-
tests/c/oracle/sum_array.res.oracle | 286 +-
tests/c/oracle/swap.res.oracle | 26 +-
tests/c/oracle/tree_max.res.oracle | 174 +-
tests/c/popHeap.c | 2 +-
tests/c/power.c | 24 +-
tests/c/sum_array.c | 8 +-
tests/java/BankingExample.java | 26 +
tests/java/BinarySearch.java | 5 +-
.../{BinarySearch.java => BinarySearchWrong.java} | 2 +-
tests/java/MyCosine.java | 1 +
tests/java/oracle/AllZeros.res.oracle | 26 +-
tests/java/oracle/ArrayMax.res.oracle | 237 +-
tests/java/oracle/Arrays.res.oracle | 26 +-
tests/java/oracle/Assertion.res.oracle | 67 +-
tests/java/oracle/BinarySearch.res.oracle | 26 +-
tests/java/oracle/Bug_sort_exns.res.oracle | 45 +-
tests/java/oracle/Counter.res.oracle | 26 +-
tests/java/oracle/Creation.res.oracle | 26 +-
tests/java/oracle/Duplets.res.oracle | 147 +-
tests/java/oracle/Fact.res.oracle | 128 +-
tests/java/oracle/Fibonacci.res.oracle | 26 +-
tests/java/oracle/FlagStatic.res.oracle | 26 +-
tests/java/oracle/Fresh.res.oracle | 82 +-
tests/java/oracle/Fresh2.res.oracle | 168 +-
tests/java/oracle/Fresh3.res.oracle | 160 +-
tests/java/oracle/Gcd.res.oracle | 26 +-
tests/java/oracle/Hello.res.oracle | 26 +-
tests/java/oracle/Isqrt.res.oracle | 26 +-
tests/java/oracle/Literals.res.oracle | 26 +-
tests/java/oracle/MacCarthy.res.oracle | 26 +-
tests/java/oracle/Muller.res.oracle | 26 +-
tests/java/oracle/MullerTheory.res.oracle | 26 +-
tests/java/oracle/MyCosine.res.oracle | 26 +-
tests/java/oracle/NameConflicts.res.oracle | 26 +-
tests/java/oracle/Negate.res.oracle | 26 +-
tests/java/oracle/Power.res.oracle | 238 +-
tests/java/oracle/PreAndOld.res.oracle | 26 +-
tests/java/oracle/Purse.res.oracle | 26 +-
tests/java/oracle/SelectionSort.res.oracle | 26 +-
tests/java/oracle/SideEffects.res.oracle | 26 +-
tests/java/oracle/SimpleAlloc.res.oracle | 26 +-
tests/java/oracle/SimpleApplet.res.oracle | 26 +-
tests/java/oracle/Sort.res.oracle | 26 +-
tests/java/oracle/Sort2.res.oracle | 26 +-
tests/java/oracle/Switch.res.oracle | 26 +-
tests/java/oracle/Termination.res.oracle | 26 +-
tests/java/oracle/TestNonNull.res.oracle | 26 +-
tests/java/oracle/TreeMax.res.oracle | 144 +-
tests/java/oracle/bts15964.res.oracle | 34 +-
tools/cvcl_split.mll | 3 +-
tools/dp.ml | 34 +-
tools/ergo_split.mll | 3 +-
tools/rv_split.mll | 1 -
tools/simplify_lexer.mll | 2 -
tools/simplify_split.mll | 1 -
tools/smtlib_split.mll | 1 -
tools/toolstat_pars.mly | 29 +-
tools/whystat.ml | 1 -
tools/zenon_split.mll | 1 -
237 files changed, 10214 insertions(+), 6168 deletions(-)
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git
More information about the Pkg-ocaml-maint-commits
mailing list