This is an automated email from the git hooks/post-receive script.

treinen pushed a change to branch upstream
in repository why.

      from  9904cd2   Imported Upstream version 2.30+dfsg
      adds  d95adde   Imported Upstream version 2.33

No new revisions were added by this update.

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 +-
 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 +
 274 files changed, 136730 insertions(+), 51280 deletions(-)
 mode change 100644 => 100755 bench/jc/bench
 create mode 100644 bench/jc/good/Sbox.jc
 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

_______________________________________________
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

Reply via email to