[Pkg-ocaml-maint-commits] [why] branch master updated (6691a9d -> a5cb0d0)
Ralf Treinen
treinen at moszumanska.debian.org
Fri Jan 17 21:12:35 UTC 2014
This is an automated email from the git hooks/post-receive script.
treinen pushed a change to branch master
in repository why.
from 6691a9d Release to unstable
new d95adde Imported Upstream version 2.33
new 4b34bdd Merge tag 'upstream/2.33'
new e25b24d drop patch 0001-Why-2.29-do-support-Coq-8.3.patch
new 3952804 drop patch 0002-Mark-alt-ergo-0.93-as-compatible.patch
new 3d31b03 drop patch 0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe
new 0d3b776 drop patch 0004-Default-to-why2-for-jessie-atp
new f45d3e7 drop patch 0005-Fix-Jc_annot_inference-use-old_reg_pos
new c390a74 drop patch 0006-Fix-spelling-error-in-binary
new e6ed240 drop patch 0007-Replace-caduceus-invocation-by-Frama-C
new 870626c drop patch 0006-Fix-spelling-error-in-binary
new 341391d replace deprecated "or" by "||"
new 631c48c add patch hashtabl to fix type error
new 50bca5c add Ralf to uploaders
new a5cb0d0 standards-version 3.9.5
The 14 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 | 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 +-
debian/changelog | 19 +
debian/control | 5 +-
.../patches/0001-Why-2.29-do-support-Coq-8.3.patch | 22 -
.../0002-Mark-alt-ergo-0.93-as-compatible.patch | 24 -
...austive-pattern-matching-in-jc_annot_infe.patch | 40 -
.../0004-Default-to-why2-for-jessie-atp.patch | 22 -
...05-Fix-Jc_annot_inference-use-old_reg_pos.patch | 22 -
.../0006-Fix-spelling-error-in-binary.patch | 36 -
...07-Replace-caduceus-invocation-by-Frama-C.patch | 24 -
debian/patches/deprecated-or | 201 +
debian/patches/hashtbl | 56 +
debian/patches/series | 9 +-
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_ge312.ml => jc_stdlib_ge40.ml} | 2 +-
jc/{jc_stdlib_ge312.ml => jc_stdlib_ge400.ml} | 2 +-
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 +-
.../c/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 +-
.../.depend => tests/c/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 +-
.../oracle/double_rounding_strict_model.err.oracle | 0
...cle => double_rounding_strict_model.res.oracle} | 1119 +-
tests/c/oracle/duplets.res.oracle | 4935 +--
.../.depend => tests/c/oracle/eps_line1.err.oracle | 0
tests/c/oracle/eps_line1.res.oracle | 3905 ++
.../.depend => tests/c/oracle/eps_line2.err.oracle | 0
tests/c/oracle/eps_line2.res.oracle | 4048 ++
.../.depend => tests/c/oracle/exp.err.oracle | 0
.../c/oracle/{minmax.res.oracle => exp.res.oracle} | 1844 +-
.../c/oracle/find_array.err.oracle | 0
tests/c/oracle/find_array.res.oracle | 5021 +++
tests/c/oracle/flag.res.oracle | 932 +-
.../c/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 +-
.../c/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 +-
.../c/oracle/overflow_level.err.oracle | 0
...erbenz.res.oracle => overflow_level.res.oracle} | 1213 +-
.../.depend => tests/c/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 +-
.../c/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 +++++-----
.../.depend => tests/c/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 +-
.../java/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 +-
.../.depend => tests/java/oracle/Fresh.err.oracle | 0
.../{NameConflicts.res.oracle => Fresh.res.oracle} | 1974 +-
.../.depend => tests/java/oracle/Fresh2.err.oracle | 0
.../{MacCarthy.res.oracle => Fresh2.res.oracle} | 2674 +-
.../.depend => tests/java/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 +-
.../.depend => tests/java/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 +
286 files changed, 137011 insertions(+), 51479 deletions(-)
mode change 100644 => 100755 bench/jc/bench
create mode 100644 bench/jc/good/Sbox.jc
delete mode 100644 debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
delete mode 100644 debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
delete mode 100644 debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
delete mode 100644 debian/patches/0004-Default-to-why2-for-jessie-atp.patch
delete mode 100644 debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
delete mode 100644 debian/patches/0006-Fix-spelling-error-in-binary.patch
delete mode 100644 debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch
create mode 100644 debian/patches/deprecated-or
create mode 100644 debian/patches/hashtbl
rename frama-c-plugin/{integer.ml => jessie_integer.ml} (100%)
delete mode 100644 frama-c-plugin/ptests_local_config.ml
copy jc/{jc_stdlib_ge312.ml => jc_stdlib_ge40.ml} (99%)
copy jc/{jc_stdlib_ge312.ml => jc_stdlib_ge400.ml} (99%)
create mode 100644 lib/coq/Jessie_memory_model.v
create mode 100644 lib/why3/coq.drv
create mode 100644 lib/why3/jessie3_integer.why
rename lib/why3/{jessie3.why => jessie3theories.why} (95%)
create mode 100644 src/why3_kw.ml
create mode 100644 src/why3_kw.mli
delete mode 100644 tests/c/Sterbenz.jessie/coq/floats_strict_why.v
create mode 100644 tests/c/array_double.c
create mode 100644 tests/c/cd1d.c
create mode 100644 tests/c/conjugate.c
create mode 100644 tests/c/double_rounding_multirounding_model.c
create mode 100644 tests/c/double_rounding_strict_model.c
create mode 100644 tests/c/eps_line1.c
create mode 100644 tests/c/eps_line2.c
create mode 100644 tests/c/exp.c
create mode 100644 tests/c/find_array.c
create mode 100644 tests/c/float_array.c
create mode 100644 tests/c/interval_arith.c
delete mode 100644 tests/c/my_cosine.jessie/coq/floats_strict_why.v
copy examples/algo-63-64-65/.depend => tests/c/oracle/array_double.err.oracle (100%)
copy tests/c/oracle/{clock_drift.res.oracle => array_double.res.oracle} (52%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/cd1d.err.oracle (100%)
copy tests/c/oracle/{minmax.res.oracle => cd1d.res.oracle} (68%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/double_rounding_multirounding_model.err.oracle (100%)
copy tests/c/oracle/{Sterbenz.res.oracle => double_rounding_multirounding_model.res.oracle} (63%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/double_rounding_strict_model.err.oracle (100%)
copy tests/c/oracle/{Sterbenz.res.oracle => double_rounding_strict_model.res.oracle} (71%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/eps_line1.err.oracle (100%)
create mode 100644 tests/c/oracle/eps_line1.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/eps_line2.err.oracle (100%)
create mode 100644 tests/c/oracle/eps_line2.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/exp.err.oracle (100%)
copy tests/c/oracle/{minmax.res.oracle => exp.res.oracle} (66%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/find_array.err.oracle (100%)
create mode 100644 tests/c/oracle/find_array.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/float_array.err.oracle (100%)
create mode 100644 tests/c/oracle/float_array.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/interval_arith.err.oracle (100%)
create mode 100644 tests/c/oracle/interval_arith.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/overflow_level.err.oracle (100%)
copy tests/c/oracle/{Sterbenz.res.oracle => overflow_level.res.oracle} (71%)
copy examples/algo-63-64-65/.depend => tests/c/oracle/popHeap.err.oracle (100%)
create mode 100644 tests/c/oracle/popHeap.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/scalar_product.err.oracle (100%)
create mode 100644 tests/c/oracle/scalar_product.res.oracle
copy examples/algo-63-64-65/.depend => tests/c/oracle/sum_array.err.oracle (100%)
create mode 100644 tests/c/oracle/sum_array.res.oracle
create mode 100644 tests/c/overflow_level.c
create mode 100644 tests/c/popHeap.c
create mode 100644 tests/c/scalar_product.c
create mode 100644 tests/c/sum_array.c
create mode 100644 tests/java/Assertion.java
create mode 100644 tests/java/Fact.java
create mode 100644 tests/java/Fresh.java
create mode 100644 tests/java/Fresh2.java
create mode 100644 tests/java/Fresh3.java
create mode 100644 tests/java/Power.java
copy examples/algo-63-64-65/.depend => tests/java/oracle/Assertion.err.oracle (100%)
copy tests/java/oracle/{Literals.res.oracle => Assertion.res.oracle} (90%)
create mode 100644 tests/java/oracle/Fact.err.oracle
copy tests/java/oracle/{PreAndOld.res.oracle => Fact.res.oracle} (82%)
copy examples/algo-63-64-65/.depend => tests/java/oracle/Fresh.err.oracle (100%)
copy tests/java/oracle/{NameConflicts.res.oracle => Fresh.res.oracle} (80%)
copy examples/algo-63-64-65/.depend => tests/java/oracle/Fresh2.err.oracle (100%)
copy tests/java/oracle/{MacCarthy.res.oracle => Fresh2.res.oracle} (78%)
copy examples/algo-63-64-65/.depend => tests/java/oracle/Fresh3.err.oracle (100%)
copy tests/java/oracle/{MacCarthy.res.oracle => Fresh3.res.oracle} (65%)
copy examples/algo-63-64-65/.depend => tests/java/oracle/Power.err.oracle (100%)
copy tests/java/oracle/{Isqrt.res.oracle => Power.res.oracle} (73%)
--
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