[Pkg-ocaml-maint-commits] [why] 02/14: Merge tag 'upstream/2.33'
Ralf Treinen
treinen at moszumanska.debian.org
Fri Jan 17 21:12:40 UTC 2014
This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository why.
commit 4b34bddba2966517de011d5ef374c23c28badb3d
Merge: 6691a9d d95adde
Author: Ralf Treinen <treinen at free.fr>
Date: Fri Jan 17 20:01:54 2014 +0100
Merge tag 'upstream/2.33'
Upstream version 2.33
.depend | 55 +-
.depend.coq | 1 +
CHANGES | 30 +-
Makefile.in | 65 +-
Version | 2 +-
bench/jc/bench | 2 +-
bench/jc/good/Sbox.jc | 780 +
bin/gwhy.sh | 6 +-
configure | 289 +-
configure.in | 34 +-
doc/Makefile | 4 +-
examples/sqrt/sqrt_why.v | 2 +-
frama-c-plugin/Makefile | 4 +-
frama-c-plugin/common.ml | 624 +-
frama-c-plugin/common.mli | 39 +-
frama-c-plugin/interp.ml | 608 +-
frama-c-plugin/{integer.ml => jessie_integer.ml} | 0
frama-c-plugin/jessie_options.ml | 26 +-
frama-c-plugin/norm.ml | 266 +-
frama-c-plugin/norm.mli | 2 +
frama-c-plugin/ptests_local_config.ml | 6 -
frama-c-plugin/register.ml | 80 +-
frama-c-plugin/retype.ml | 20 +-
frama-c-plugin/rewrite.ml | 791 +-
frama-c-plugin/share/jessie/jessie_prolog.h | 4 +-
frama-c-plugin/share/jessie/stdio.h | 2 +-
frama-c-plugin/share/jessie/stdlib.h | 12 +-
frama-c-plugin/share/jessie/string.h | 30 +-
frama-c-plugin/share/jessie/strings.h | 4 +-
frama-c-plugin/share/jessie/unistd.h | 2 +-
frama-c-plugin/share/jessie/wchar.h | 8 +-
java/java_analysis.ml | 3 +-
java/java_ast.mli | 93 +-
java/java_callgraph.ml | 195 +-
java/java_interp.ml | 11 +-
java/java_lexer.mll | 163 +-
java/java_main.ml | 2 +-
java/java_parser.mly | 365 +-
java/java_pervasives.ml | 3 +-
java/java_tast.mli | 2 +
java/java_typing.ml | 1638 +-
java/java_typing.mli | 52 +-
jc/jc_annot_inference.ml | 1238 +-
jc/jc_ast.mli | 143 +-
jc/jc_callgraph.ml | 15 +-
jc/jc_callgraph.mli | 6 +-
jc/jc_constructors.ml | 30 +-
jc/jc_constructors.mli | 11 +
jc/jc_effect.ml | 181 +-
jc/jc_envset.ml | 3 +-
jc/jc_fenv.ml | 3 -
jc/jc_frame.ml | 228 +-
jc/jc_frame_notin.ml | 2 +-
jc/jc_interp.ml | 96 +-
jc/jc_interp_misc.ml | 23 +-
jc/jc_interp_misc.mli | 8 +-
jc/jc_invariants.ml | 44 +-
jc/jc_iterators.ml | 17 +
jc/jc_iterators.mli | 2 +
jc/jc_lexer.mll | 18 +-
jc/jc_main.ml | 73 +-
jc/jc_make.ml | 24 +-
jc/jc_norm.ml | 142 +-
jc/jc_noutput.ml | 2 +
jc/jc_options.ml | 8 +-
jc/jc_options.mli | 2 +-
jc/jc_output.ml | 3 +
jc/jc_parser.mly | 32 +-
jc/jc_pattern.ml | 5 +-
jc/jc_pervasives.ml | 291 +-
jc/jc_pervasives.mli | 22 +
jc/jc_poutput.ml | 194 +-
jc/jc_separation.ml | 138 +-
jc/jc_stdlib_ge40.ml | 260 +
jc/jc_stdlib_ge400.ml | 260 +
jc/jc_typing.ml | 238 +-
jc/jc_typing.mli | 39 +-
jc/output.ml | 490 +-
jc/output.mli | 13 +-
lib/coq/Jessie_memory_model.v | 979 +
lib/coq/WhyFloats.v | 187 +-
lib/coq/WhyTuples.v | 2 +-
lib/coq/jessie_why.v | 45 +-
lib/why/floats_multi_rounding.why | 6 +
lib/why/jessie.why | 7 +-
lib/why/real.why | 65 +-
lib/why3/coq.drv | 3 +
lib/why3/jessie3.mlw | 740 +-
lib/why3/jessie3_integer.why | 112 +
lib/why3/{jessie3.why => jessie3theories.why} | 35 +-
mix/mix_cfg.ml | 2 +-
mix/mix_seq.ml | 6 +-
src/encoding_pred.ml | 4 +-
src/encoding_rec.ml | 4 +-
src/pretty.ml | 142 +-
src/smtlib.ml | 2 +-
src/theory_filtering.ml | 4 +-
src/theoryreducer.ml | 2 +
src/vcg.ml | 4 +-
src/why3.ml | 70 +-
src/why3_kw.ml | 67 +
src/why3_kw.mli | 3 +
tests/c/Sterbenz.c | 2 +-
tests/c/Sterbenz.jessie/coq/Sterbenz_why.v | 89 +
tests/c/Sterbenz.jessie/coq/floats_strict_why.v | 289 -
tests/c/array_double.c | 30 +
tests/c/array_max.c | 2 +-
tests/c/binary_heap.c | 5 +-
tests/c/binary_search.c | 4 +-
tests/c/cd1d.c | 24 +
tests/c/clock_drift.c | 2 +-
tests/c/conjugate.c | 80 +
tests/c/double_rounding_multirounding_model.c | 24 +
tests/c/double_rounding_strict_model.c | 16 +
tests/c/duplets.c | 2 +-
tests/c/eps_line1.c | 43 +
tests/c/eps_line2.c | 44 +
tests/c/exp.c | 17 +
tests/c/find_array.c | 50 +
tests/c/flag.c | 2 +-
tests/c/float_array.c | 60 +
tests/c/float_sqrt.c | 2 +-
tests/c/floats_bsearch.c | 2 +-
tests/c/insertion_sort.c | 4 +-
tests/c/interval_arith.c | 263 +
tests/c/isqrt.c | 2 +-
tests/c/minmax.c | 2 +-
tests/c/muller.c | 10 +-
tests/c/my_cosine.c | 9 +-
tests/c/my_cosine.jessie/coq/floats_strict_why.v | 289 -
tests/c/my_cosine.jessie/coq/my_cosine_why.v | 135 +-
tests/c/oracle/Sterbenz.err.oracle | 2 +
tests/c/oracle/Sterbenz.res.oracle | 377 +-
...Sterbenz.err.oracle => array_double.err.oracle} | 0
...ck_drift.res.oracle => array_double.res.oracle} | 2618 +-
tests/c/oracle/array_max.res.oracle | 541 +-
tests/c/oracle/binary_heap.res.oracle | 1671 +-
tests/c/oracle/binary_search.res.oracle | 2189 +-
.../{Sterbenz.err.oracle => cd1d.err.oracle} | 0
.../oracle/{minmax.res.oracle => cd1d.res.oracle} | 1811 +-
tests/c/oracle/clock_drift.res.oracle | 1052 +-
...double_rounding_multirounding_model.err.oracle} | 0
...double_rounding_multirounding_model.res.oracle} | 1385 +-
...cle => double_rounding_strict_model.err.oracle} | 0
...cle => double_rounding_strict_model.res.oracle} | 1119 +-
tests/c/oracle/duplets.res.oracle | 4935 +--
.../{Sterbenz.err.oracle => eps_line1.err.oracle} | 0
tests/c/oracle/eps_line1.res.oracle | 3905 ++
.../{Sterbenz.err.oracle => eps_line2.err.oracle} | 0
tests/c/oracle/eps_line2.res.oracle | 4048 ++
.../oracle/{Sterbenz.err.oracle => exp.err.oracle} | 0
.../c/oracle/{minmax.res.oracle => exp.res.oracle} | 1844 +-
.../{Sterbenz.err.oracle => find_array.err.oracle} | 0
tests/c/oracle/find_array.res.oracle | 5021 +++
tests/c/oracle/flag.res.oracle | 932 +-
...{Sterbenz.err.oracle => float_array.err.oracle} | 0
tests/c/oracle/float_array.res.oracle | 4205 +++
tests/c/oracle/float_sqrt.res.oracle | 556 +-
tests/c/oracle/floats_bsearch.res.oracle | 1913 +-
tests/c/oracle/heap_sort.res.oracle | 1352 +-
tests/c/oracle/insertion_sort.res.oracle | 3470 +-
...erbenz.err.oracle => interval_arith.err.oracle} | 0
tests/c/oracle/interval_arith.res.oracle | 14930 ++++++++
tests/c/oracle/isqrt.res.oracle | 215 +-
tests/c/oracle/maze.res.oracle | 2 +-
tests/c/oracle/minmax.res.oracle | 248 +-
tests/c/oracle/muller.res.oracle | 5420 +--
tests/c/oracle/my_cosine.res.oracle | 1460 +-
...erbenz.err.oracle => overflow_level.err.oracle} | 0
...erbenz.res.oracle => overflow_level.res.oracle} | 1213 +-
.../{Sterbenz.err.oracle => popHeap.err.oracle} | 0
tests/c/oracle/popHeap.res.oracle | 37371 +++++++++++++++++++
tests/c/oracle/quick_sort.res.oracle | 4765 +--
tests/c/oracle/rec.res.oracle | 635 +-
...erbenz.err.oracle => scalar_product.err.oracle} | 0
tests/c/oracle/scalar_product.res.oracle | 5591 +++
tests/c/oracle/selection_sort.res.oracle | 3837 +-
tests/c/oracle/sparse_array.res.oracle | 6530 +---
tests/c/oracle/sparse_array2.res.oracle | 20603 +++++-----
.../{Sterbenz.err.oracle => sum_array.err.oracle} | 0
tests/c/oracle/sum_array.res.oracle | 3878 ++
tests/c/oracle/swap.res.oracle | 246 +-
tests/c/oracle/tree_max.res.oracle | 264 +-
tests/c/overflow_level.c | 9 +
tests/c/popHeap.c | 256 +
tests/c/quick_sort.c | 2 +-
tests/c/rec.c | 2 +-
tests/c/scalar_product.c | 93 +
tests/c/sparse_array.c | 4 +-
tests/c/sparse_array2.c | 14 +-
tests/c/sum_array.c | 67 +
tests/c/tree_max.c | 8 +
tests/java/AllZeros.java | 2 +-
tests/java/ArrayMax.java | 2 +-
tests/java/Arrays.java | 2 +-
tests/java/Assertion.java | 9 +
tests/java/BinarySearch.java | 2 +-
tests/java/Counter.java | 2 +-
tests/java/Creation.java | 2 +-
tests/java/Duplets.java | 2 +-
tests/java/Fact.java | 27 +
tests/java/Fibonacci.java | 2 +-
tests/java/FlagStatic.java | 2 +-
tests/java/Fresh.java | 27 +
tests/java/Fresh2.java | 40 +
tests/java/Fresh3.java | 40 +
tests/java/Gcd.java | 4 +-
tests/java/Hello.java | 2 +-
tests/java/Isqrt.java | 2 +-
tests/java/Literals.java | 2 +-
tests/java/MacCarthy.java | 2 +-
tests/java/Muller.java | 6 +-
tests/java/NameConflicts.java | 2 +-
tests/java/Negate.java | 2 +-
tests/java/Power.java | 65 +
tests/java/PreAndOld.java | 2 +-
tests/java/Purse.java | 2 +-
tests/java/SelectionSort.java | 2 +-
tests/java/SideEffects.java | 2 +-
tests/java/SimpleAlloc.java | 2 +-
tests/java/SimpleApplet.java | 2 +-
tests/java/Switch.java | 2 +-
tests/java/Termination.java | 2 +-
tests/java/TestNonNull.java | 2 +-
tests/java/coq/Fibonacci_why.v | 5 -
tests/java/oracle/AllZeros.res.oracle | 106 +-
tests/java/oracle/ArrayMax.res.oracle | 106 +-
tests/java/oracle/Arrays.res.oracle | 101 +-
.../oracle/Assertion.err.oracle} | 0
.../{Literals.res.oracle => Assertion.res.oracle} | 771 +-
tests/java/oracle/BinarySearch.res.oracle | 129 +-
tests/java/oracle/Counter.res.oracle | 83 +-
tests/java/oracle/Creation.res.oracle | 155 +-
tests/java/oracle/Duplets.err.oracle | 4 +-
tests/java/oracle/Duplets.res.oracle | 2 +-
tests/java/oracle/Fact.err.oracle | 3 +
.../{PreAndOld.res.oracle => Fact.res.oracle} | 1388 +-
tests/java/oracle/Fibonacci.res.oracle | 88 +-
tests/java/oracle/FlagStatic.res.oracle | 89 +-
.../oracle/Fresh.err.oracle} | 0
.../{NameConflicts.res.oracle => Fresh.res.oracle} | 1974 +-
.../oracle/Fresh2.err.oracle} | 0
.../{MacCarthy.res.oracle => Fresh2.res.oracle} | 2674 +-
.../oracle/Fresh3.err.oracle} | 0
.../{MacCarthy.res.oracle => Fresh3.res.oracle} | 3789 +-
tests/java/oracle/Gcd.res.oracle | 168 +-
tests/java/oracle/Hello.res.oracle | 3645 +-
tests/java/oracle/Isqrt.res.oracle | 83 +-
tests/java/oracle/Literals.res.oracle | 106 +-
tests/java/oracle/MacCarthy.res.oracle | 106 +-
tests/java/oracle/Muller.res.oracle | 413 +-
tests/java/oracle/MullerTheory.res.oracle | 81 +-
tests/java/oracle/NameConflicts.res.oracle | 106 +-
tests/java/oracle/Negate.res.oracle | 83 +-
.../oracle/Power.err.oracle} | 0
.../oracle/{Isqrt.res.oracle => Power.res.oracle} | 3264 +-
tests/java/oracle/PreAndOld.res.oracle | 83 +-
tests/java/oracle/Purse.res.oracle | 83 +-
tests/java/oracle/SelectionSort.res.oracle | 239 +-
tests/java/oracle/SideEffects.res.oracle | 83 +-
tests/java/oracle/SimpleAlloc.res.oracle | 106 +-
tests/java/oracle/SimpleApplet.res.oracle | 118 +-
tests/java/oracle/Sort.res.oracle | 87 +-
tests/java/oracle/Sort2.res.oracle | 87 +-
tests/java/oracle/Switch.res.oracle | 106 +-
tests/java/oracle/Termination.res.oracle | 83 +-
tests/java/oracle/TestNonNull.res.oracle | 133 +-
tests/java/oracle/TreeMax.res.oracle | 104 +-
tests/regtest.sh | 20 +-
tools/calldp.ml | 70 +-
tools/calldp.mli | 33 +-
tools/dp.ml | 35 +-
tools/dpConfig.ml | 34 +-
tools/regtest.ml | 2 +
274 files changed, 137248 insertions(+), 51278 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