diff --git a/HACKING.md b/HACKING.md index fcc31651c2..bc939f426c 100644 --- a/HACKING.md +++ b/HACKING.md @@ -51,7 +51,7 @@ If the proof of a test is broken (e.g. ./ide creusot/tests/should_succeed/cell/01 ``` -## Calling why3 & why3_tools: shell environment setup +## Calling why3 (and why3_tools, etc): shell environment setup To invoke why3 (manually or in scripts) with the same binary/configuration as setup by `cargo creusot setup`, one needs to setup a shell environment with the @@ -66,7 +66,7 @@ After that, the `why3` binary in PATH will be the one configured by `cargo creusot setup`, using the adequate configuration file (through the `WHY3CONFIG` environment variable). -## Upgrading the revision of Why3 used by Creusot +## Upgrading Why3 Edit `creusot-deps.opam` to use the hash of the git commit of the latest commit in Why3's master branch. (But first make sure that the Nightly CI job passes.) @@ -74,3 +74,13 @@ in Why3's master branch. (But first make sure that the Nightly CI job passes.) There are several places to edit in the file: the `pin-depends` field at the end of the file (URLs and `git-XXXX` versions), and the `git-XXXX` versions in the `depends:` field. + +## Upgrading a prover to a newer version + +- Install why3-tools: `opam pin git+https://github.com/xldenis/why3-tools` +- Install the newer prover, make it available in `$PATH` +- Setup Creusot to use it: `cargo creusot setup install --no-check-version --external ` +- Run `eval $(cargo run --bin dev-env)` +- Use the `./testsuite_upgrade_prover` script to update why3 sessions in the testsuite. + Launch the script without arguments to have some usage instructions. +- Once the testsuite is migrated, update `creusot-setup/src/{tools,tools_versions_urls}.rs` diff --git a/ci/creusot-deps-nightly.opam b/ci/creusot-deps-nightly.opam index 98ce304185..da441c6ada 100644 --- a/ci/creusot-deps-nightly.opam +++ b/ci/creusot-deps-nightly.opam @@ -10,7 +10,7 @@ depends: [ "camlzip" "zarith" # the alt-ergo solver - "alt-ergo" {= "2.4.3"} + "alt-ergo" {= "2.5.3"} ] pin-depends: [ [ "why3.git" "git+https://gitlab.inria.fr/why3/why3.git" ] diff --git a/creusot-deps.opam b/creusot-deps.opam index 9617013425..903d1ddb78 100644 --- a/creusot-deps.opam +++ b/creusot-deps.opam @@ -11,7 +11,7 @@ depends: [ "camlzip" "zarith" # the alt-ergo solver - "alt-ergo" {= "2.4.3"} + "alt-ergo" {= "2.5.3"} ] # When updating the hash and git-XXX below, don't forget to update them in the # depends: field above! diff --git a/creusot-setup/src/tools.rs b/creusot-setup/src/tools.rs index 7ec6ee97a5..c357368fb6 100644 --- a/creusot-setup/src/tools.rs +++ b/creusot-setup/src/tools.rs @@ -215,9 +215,7 @@ pub fn generate_why3_conf( fn detect_altergo_version(altergo: &Path) -> Option { let output = Command::new(&altergo).arg("--version").output().ok()?; let out_s = String::from_utf8(output.stdout).ok()?; - // will be needed for more recent altergo versions - // out_s.trim_end().strip_prefix("v").map(String::from) - Some(out_s.trim_end().to_owned()) + out_s.trim_end().strip_prefix("v").map(String::from) } // helpers: Z3 diff --git a/creusot-setup/src/tools_versions_urls.rs b/creusot-setup/src/tools_versions_urls.rs index 3333a31a14..c1621b46cc 100644 --- a/creusot-setup/src/tools_versions_urls.rs +++ b/creusot-setup/src/tools_versions_urls.rs @@ -7,7 +7,7 @@ // tools without binary releases pub const WHY3_VERSION: &'static str = "1.7.1"; -pub const ALTERGO_VERSION: &'static str = "2.4.3"; +pub const ALTERGO_VERSION: &'static str = "2.5.3"; // tools with binary releases pub const Z3_VERSION: &'static str = "4.12.4"; pub const CVC4_VERSION: &'static str = "1.8"; diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml index 213d020e8a..a83d643e15 100644 --- a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml +++ b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -12,34 +12,38 @@ - + - + - - - - - + + + + + - - - - - - - - + + + + + + + + - - - - + + + + + + + + diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz index db7e9d943d..eab001e49c 100644 Binary files a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz and b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/222/why3session.xml b/creusot/tests/should_fail/bug/222/why3session.xml index 9932edc3c3..3e8e8e7a07 100644 --- a/creusot/tests/should_fail/bug/222/why3session.xml +++ b/creusot/tests/should_fail/bug/222/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -9,15 +9,15 @@ - - - - + + + + - - - + + + diff --git a/creusot/tests/should_fail/bug/222/why3shapes.gz b/creusot/tests/should_fail/bug/222/why3shapes.gz index 2c910b62d0..cadd2144b8 100644 Binary files a/creusot/tests/should_fail/bug/222/why3shapes.gz and b/creusot/tests/should_fail/bug/222/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/492/why3session.xml b/creusot/tests/should_fail/bug/492/why3session.xml index 8bc1570b31..3eb7a6d5fe 100644 --- a/creusot/tests/should_fail/bug/492/why3session.xml +++ b/creusot/tests/should_fail/bug/492/why3session.xml @@ -1,22 +1,22 @@ +"https://www.why3.org/why3session.dtd"> - - - + + + - - - + + + diff --git a/creusot/tests/should_fail/bug/492/why3shapes.gz b/creusot/tests/should_fail/bug/492/why3shapes.gz index 8e0aca45dd..6197c36c5c 100644 Binary files a/creusot/tests/should_fail/bug/492/why3shapes.gz and b/creusot/tests/should_fail/bug/492/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/692/why3session.xml b/creusot/tests/should_fail/bug/692/why3session.xml index 354ffdfa03..e2b34182e8 100644 --- a/creusot/tests/should_fail/bug/692/why3session.xml +++ b/creusot/tests/should_fail/bug/692/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -10,25 +10,25 @@ - - - - + + + + - - - + + + - - - + + + - - - + + + diff --git a/creusot/tests/should_fail/bug/692/why3shapes.gz b/creusot/tests/should_fail/bug/692/why3shapes.gz index a21a0e34b8..c21f76c031 100644 Binary files a/creusot/tests/should_fail/bug/692/why3shapes.gz and b/creusot/tests/should_fail/bug/692/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/695/why3session.xml b/creusot/tests/should_fail/bug/695/why3session.xml index a0bd8d4868..91e5eb0463 100644 --- a/creusot/tests/should_fail/bug/695/why3session.xml +++ b/creusot/tests/should_fail/bug/695/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -8,27 +8,27 @@ - - - + + + - - - + + + - - - + + + - - - - + + + + diff --git a/creusot/tests/should_fail/bug/695/why3shapes.gz b/creusot/tests/should_fail/bug/695/why3shapes.gz index e1f52d49f0..b76fb7262d 100644 Binary files a/creusot/tests/should_fail/bug/695/why3shapes.gz and b/creusot/tests/should_fail/bug/695/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/869/why3session.xml b/creusot/tests/should_fail/bug/869/why3session.xml index 792fb12aa4..13f7b97be9 100644 --- a/creusot/tests/should_fail/bug/869/why3session.xml +++ b/creusot/tests/should_fail/bug/869/why3session.xml @@ -1,45 +1,73 @@ +"https://www.why3.org/why3session.dtd"> - + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - + + + + - + - - - - + + + + - + - + diff --git a/creusot/tests/should_fail/bug/869/why3shapes.gz b/creusot/tests/should_fail/bug/869/why3shapes.gz index 54a393a5e3..f1c6c99967 100644 Binary files a/creusot/tests/should_fail/bug/869/why3shapes.gz and b/creusot/tests/should_fail/bug/869/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/specialize/why3session.xml b/creusot/tests/should_fail/bug/specialize/why3session.xml index 53dd686f19..221e210bf3 100644 --- a/creusot/tests/should_fail/bug/specialize/why3session.xml +++ b/creusot/tests/should_fail/bug/specialize/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -11,22 +11,30 @@ - - - - + + + + - - - + + + - - - + + + + + + + + + + + diff --git a/creusot/tests/should_fail/bug/specialize/why3shapes.gz b/creusot/tests/should_fail/bug/specialize/why3shapes.gz index b609a478c7..faed9c95d8 100644 Binary files a/creusot/tests/should_fail/bug/specialize/why3shapes.gz and b/creusot/tests/should_fail/bug/specialize/why3shapes.gz differ diff --git a/creusot/tests/should_fail/bug/subregion/why3session.xml b/creusot/tests/should_fail/bug/subregion/why3session.xml index ebb050ee6e..058db0051f 100644 --- a/creusot/tests/should_fail/bug/subregion/why3session.xml +++ b/creusot/tests/should_fail/bug/subregion/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -9,15 +9,15 @@ - - + + - - + + - - + + diff --git a/creusot/tests/should_fail/bug/subregion/why3shapes.gz b/creusot/tests/should_fail/bug/subregion/why3shapes.gz index f95a9d5011..34bdd5b505 100644 Binary files a/creusot/tests/should_fail/bug/subregion/why3shapes.gz and b/creusot/tests/should_fail/bug/subregion/why3shapes.gz differ diff --git a/creusot/tests/should_fail/final_borrows/why3session.xml b/creusot/tests/should_fail/final_borrows/why3session.xml index 42ce63e43a..97fb6221a4 100644 --- a/creusot/tests/should_fail/final_borrows/why3session.xml +++ b/creusot/tests/should_fail/final_borrows/why3session.xml @@ -1,75 +1,75 @@ +"https://www.why3.org/why3session.dtd"> - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - + + + + - - - - + + + + @@ -79,62 +79,62 @@ - + - + - + - + - + - + - - - - + + + + - + - + - + - + - + - + - - - - + + + + - + diff --git a/creusot/tests/should_fail/final_borrows/why3shapes.gz b/creusot/tests/should_fail/final_borrows/why3shapes.gz index f162bf2718..ea367b2fef 100644 Binary files a/creusot/tests/should_fail/final_borrows/why3shapes.gz and b/creusot/tests/should_fail/final_borrows/why3shapes.gz differ diff --git a/creusot/tests/should_fail/opaque_unproveable/why3session.xml b/creusot/tests/should_fail/opaque_unproveable/why3session.xml index 640fa74bee..e73a912032 100644 --- a/creusot/tests/should_fail/opaque_unproveable/why3session.xml +++ b/creusot/tests/should_fail/opaque_unproveable/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> @@ -10,10 +10,10 @@ - - - - + + + + diff --git a/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz b/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz index e91fe1a00f..3e2028270a 100644 Binary files a/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz and b/creusot/tests/should_fail/opaque_unproveable/why3shapes.gz differ diff --git a/creusot/tests/should_fail/traits/17_impl_refinement/why3session.xml b/creusot/tests/should_fail/traits/17_impl_refinement/why3session.xml index dbd127a5cf..b6b3858372 100644 --- a/creusot/tests/should_fail/traits/17_impl_refinement/why3session.xml +++ b/creusot/tests/should_fail/traits/17_impl_refinement/why3session.xml @@ -1,23 +1,27 @@ +"https://www.why3.org/why3session.dtd"> - - - + + + - - - + + + + + + + - + diff --git a/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz b/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz index a9bf401863..6ea53a67c8 100644 Binary files a/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz and b/creusot/tests/should_fail/traits/17_impl_refinement/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/100doors/why3shapes.gz b/creusot/tests/should_succeed/100doors/why3shapes.gz index 8070c69fdf..5b4edbe5ee 100644 Binary files a/creusot/tests/should_succeed/100doors/why3shapes.gz and b/creusot/tests/should_succeed/100doors/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/all_zero/why3session.xml b/creusot/tests/should_succeed/all_zero/why3session.xml index 56e15c6ed6..4ff9b94a06 100644 --- a/creusot/tests/should_succeed/all_zero/why3session.xml +++ b/creusot/tests/should_succeed/all_zero/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bdd/why3session.xml b/creusot/tests/should_succeed/bdd/why3session.xml index be8a0fe45b..d2d42a2f1a 100644 --- a/creusot/tests/should_succeed/bdd/why3session.xml +++ b/creusot/tests/should_succeed/bdd/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -19,7 +19,7 @@ - + @@ -29,7 +29,7 @@ - + @@ -49,40 +49,40 @@ - + - + - + - + - + - + - + - + - + - + @@ -91,146 +91,146 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -242,14 +242,14 @@ - + - + @@ -275,22 +275,22 @@ - + - + - + - + - + - + @@ -305,16 +305,16 @@ - + - + - + @@ -361,7 +361,7 @@ - + @@ -390,52 +390,52 @@ - + - + - + - + - + - + - + - + - + - + - + @@ -445,46 +445,46 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -518,61 +518,61 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -581,19 +581,19 @@ - + - + - + - + - + @@ -655,7 +655,7 @@ - + @@ -676,16 +676,16 @@ - + - + - + @@ -815,12 +815,12 @@ - + - + diff --git a/creusot/tests/should_succeed/binary_search/why3session.xml b/creusot/tests/should_succeed/binary_search/why3session.xml index f72f0b0ff8..f973c5563a 100644 --- a/creusot/tests/should_succeed/binary_search/why3session.xml +++ b/creusot/tests/should_succeed/binary_search/why3session.xml @@ -2,95 +2,95 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/bug/173/why3session.xml b/creusot/tests/should_succeed/bug/173/why3session.xml index b7114f41f9..cd1b566e36 100644 --- a/creusot/tests/should_succeed/bug/173/why3session.xml +++ b/creusot/tests/should_succeed/bug/173/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/206/why3session.xml b/creusot/tests/should_succeed/bug/206/why3session.xml index b407b3d775..131d365414 100644 --- a/creusot/tests/should_succeed/bug/206/why3session.xml +++ b/creusot/tests/should_succeed/bug/206/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/217/why3session.xml b/creusot/tests/should_succeed/bug/217/why3session.xml index 1cdddd223a..f39d89ebc1 100644 --- a/creusot/tests/should_succeed/bug/217/why3session.xml +++ b/creusot/tests/should_succeed/bug/217/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/235/why3session.xml b/creusot/tests/should_succeed/bug/235/why3session.xml index b9ec902f19..84861ddb51 100644 --- a/creusot/tests/should_succeed/bug/235/why3session.xml +++ b/creusot/tests/should_succeed/bug/235/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/bug/271/why3session.xml b/creusot/tests/should_succeed/bug/271/why3session.xml index 56b7d6e227..5f1d0e144b 100644 --- a/creusot/tests/should_succeed/bug/271/why3session.xml +++ b/creusot/tests/should_succeed/bug/271/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> diff --git a/creusot/tests/should_succeed/bug/273/why3session.xml b/creusot/tests/should_succeed/bug/273/why3session.xml index 58a649c88a..6d37334866 100644 --- a/creusot/tests/should_succeed/bug/273/why3session.xml +++ b/creusot/tests/should_succeed/bug/273/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/bug/395/why3session.xml b/creusot/tests/should_succeed/bug/395/why3session.xml index 3c77f7b5e8..112a91726e 100644 --- a/creusot/tests/should_succeed/bug/395/why3session.xml +++ b/creusot/tests/should_succeed/bug/395/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/463/why3session.xml b/creusot/tests/should_succeed/bug/463/why3session.xml index 949c7766d3..61a30cc71d 100644 --- a/creusot/tests/should_succeed/bug/463/why3session.xml +++ b/creusot/tests/should_succeed/bug/463/why3session.xml @@ -2,17 +2,17 @@ - + - - + + - + diff --git a/creusot/tests/should_succeed/bug/463/why3shapes.gz b/creusot/tests/should_succeed/bug/463/why3shapes.gz index d1ca6a8262..682d2b3015 100644 Binary files a/creusot/tests/should_succeed/bug/463/why3shapes.gz and b/creusot/tests/should_succeed/bug/463/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/528/why3session.xml b/creusot/tests/should_succeed/bug/528/why3session.xml index 6326f789cd..2175a89adb 100644 --- a/creusot/tests/should_succeed/bug/528/why3session.xml +++ b/creusot/tests/should_succeed/bug/528/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> diff --git a/creusot/tests/should_succeed/bug/545/why3session.xml b/creusot/tests/should_succeed/bug/545/why3session.xml index 61818957df..480cc10fb5 100644 --- a/creusot/tests/should_succeed/bug/545/why3session.xml +++ b/creusot/tests/should_succeed/bug/545/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/552/why3session.xml b/creusot/tests/should_succeed/bug/552/why3session.xml index bba975ab47..be4a157630 100644 --- a/creusot/tests/should_succeed/bug/552/why3session.xml +++ b/creusot/tests/should_succeed/bug/552/why3session.xml @@ -1,18 +1,18 @@ +"https://www.why3.org/why3session.dtd"> - + - + - + diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml index 4f358e1059..8e43ef0048 100644 --- a/creusot/tests/should_succeed/bug/682/why3session.xml +++ b/creusot/tests/should_succeed/bug/682/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/874/why3session.xml b/creusot/tests/should_succeed/bug/874/why3session.xml index 03e58888cf..a8809ab9a6 100644 --- a/creusot/tests/should_succeed/bug/874/why3session.xml +++ b/creusot/tests/should_succeed/bug/874/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/874/why3shapes.gz b/creusot/tests/should_succeed/bug/874/why3shapes.gz index 53f6d90f05..456462c1fc 100644 Binary files a/creusot/tests/should_succeed/bug/874/why3shapes.gz and b/creusot/tests/should_succeed/bug/874/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/922/why3session.xml b/creusot/tests/should_succeed/bug/922/why3session.xml index 7221b0fd31..f33f9fe10b 100644 --- a/creusot/tests/should_succeed/bug/922/why3session.xml +++ b/creusot/tests/should_succeed/bug/922/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + @@ -28,7 +28,7 @@ - + diff --git a/creusot/tests/should_succeed/bug/box_borrow_resolve/why3session.xml b/creusot/tests/should_succeed/bug/box_borrow_resolve/why3session.xml index c44b106e37..6bc0ae64c3 100644 --- a/creusot/tests/should_succeed/bug/box_borrow_resolve/why3session.xml +++ b/creusot/tests/should_succeed/bug/box_borrow_resolve/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/eq_panic/why3session.xml b/creusot/tests/should_succeed/bug/eq_panic/why3session.xml index b36230b2b0..34bda331f4 100644 --- a/creusot/tests/should_succeed/bug/eq_panic/why3session.xml +++ b/creusot/tests/should_succeed/bug/eq_panic/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/bug/final_borrows/why3session.xml b/creusot/tests/should_succeed/bug/final_borrows/why3session.xml index 2f919458e1..20ba2b65ae 100644 --- a/creusot/tests/should_succeed/bug/final_borrows/why3session.xml +++ b/creusot/tests/should_succeed/bug/final_borrows/why3session.xml @@ -4,17 +4,17 @@ - + - + - + @@ -49,7 +49,7 @@ - + @@ -59,12 +59,12 @@ - + - + @@ -89,17 +89,17 @@ - + - + - + @@ -109,7 +109,7 @@ - + diff --git a/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml b/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml index 51a7a8ca24..10e0194115 100644 --- a/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml +++ b/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/bug/pure_neq/why3session.xml b/creusot/tests/should_succeed/bug/pure_neq/why3session.xml index 462f47b14d..616fa9f47c 100644 --- a/creusot/tests/should_succeed/bug/pure_neq/why3session.xml +++ b/creusot/tests/should_succeed/bug/pure_neq/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/two_phase/why3session.xml b/creusot/tests/should_succeed/bug/two_phase/why3session.xml index c539ff1337..6f770db0b2 100644 --- a/creusot/tests/should_succeed/bug/two_phase/why3session.xml +++ b/creusot/tests/should_succeed/bug/two_phase/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz b/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz index 7958141099..e3335480e4 100644 Binary files a/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz and b/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/cell/01/why3session.xml b/creusot/tests/should_succeed/cell/01/why3session.xml index 450c0bb113..80deb7caee 100644 --- a/creusot/tests/should_succeed/cell/01/why3session.xml +++ b/creusot/tests/should_succeed/cell/01/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/cell/02/why3session.xml b/creusot/tests/should_succeed/cell/02/why3session.xml index d74c9b57c2..c87157bba4 100644 --- a/creusot/tests/should_succeed/cell/02/why3session.xml +++ b/creusot/tests/should_succeed/cell/02/why3session.xml @@ -4,7 +4,7 @@ - + @@ -21,44 +21,44 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -72,7 +72,7 @@ - + @@ -87,25 +87,25 @@ - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/cell/02/why3shapes.gz b/creusot/tests/should_succeed/cell/02/why3shapes.gz index 00882d9e3b..a0fe42f3d8 100644 Binary files a/creusot/tests/should_succeed/cell/02/why3shapes.gz and b/creusot/tests/should_succeed/cell/02/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/checked_ops/why3session.xml b/creusot/tests/should_succeed/checked_ops/why3session.xml index 759ec6ca8b..8ce7831d8d 100644 --- a/creusot/tests/should_succeed/checked_ops/why3session.xml +++ b/creusot/tests/should_succeed/checked_ops/why3session.xml @@ -2,8 +2,8 @@ + - @@ -19,7 +19,7 @@ - + @@ -39,7 +39,7 @@ - + @@ -94,7 +94,7 @@ - + @@ -119,7 +119,7 @@ - + @@ -154,7 +154,7 @@ - + diff --git a/creusot/tests/should_succeed/clones/02/why3session.xml b/creusot/tests/should_succeed/clones/02/why3session.xml index 4234c5f14c..fda45da0c9 100644 --- a/creusot/tests/should_succeed/clones/02/why3session.xml +++ b/creusot/tests/should_succeed/clones/02/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/clones/03/why3session.xml b/creusot/tests/should_succeed/clones/03/why3session.xml index 1b83e3261f..35d16608d3 100644 --- a/creusot/tests/should_succeed/clones/03/why3session.xml +++ b/creusot/tests/should_succeed/clones/03/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,12 +13,12 @@ - + - + diff --git a/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml b/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml index e680c575f1..f2d4662b55 100644 --- a/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml +++ b/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml @@ -2,18 +2,18 @@ + - - + - + @@ -23,12 +23,12 @@ - + - + @@ -38,12 +38,12 @@ - + - + diff --git a/creusot/tests/should_succeed/closures/06_fn_specs/why3shapes.gz b/creusot/tests/should_succeed/closures/06_fn_specs/why3shapes.gz index 294a6c6a55..407b2b9e00 100644 Binary files a/creusot/tests/should_succeed/closures/06_fn_specs/why3shapes.gz and b/creusot/tests/should_succeed/closures/06_fn_specs/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml b/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml index 9a56579da8..679202ac14 100644 --- a/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml +++ b/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml @@ -2,17 +2,17 @@ - + - - + + - + diff --git a/creusot/tests/should_succeed/closures/07_mutable_capture/why3shapes.gz b/creusot/tests/should_succeed/closures/07_mutable_capture/why3shapes.gz index 99257d1192..73cd9e07fa 100644 Binary files a/creusot/tests/should_succeed/closures/07_mutable_capture/why3shapes.gz and b/creusot/tests/should_succeed/closures/07_mutable_capture/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/constrained_types/why3session.xml b/creusot/tests/should_succeed/constrained_types/why3session.xml index f0b19d75ec..0169fdc76c 100644 --- a/creusot/tests/should_succeed/constrained_types/why3session.xml +++ b/creusot/tests/should_succeed/constrained_types/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/drop_pair/why3session.xml b/creusot/tests/should_succeed/drop_pair/why3session.xml index 4c9ae6e966..06ba25b083 100644 --- a/creusot/tests/should_succeed/drop_pair/why3session.xml +++ b/creusot/tests/should_succeed/drop_pair/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/filter_positive/why3session.xml b/creusot/tests/should_succeed/filter_positive/why3session.xml index 8d1abbb75a..c11b1a7292 100644 --- a/creusot/tests/should_succeed/filter_positive/why3session.xml +++ b/creusot/tests/should_succeed/filter_positive/why3session.xml @@ -3,12 +3,12 @@ "https://www.why3.org/why3session.dtd"> - + - + @@ -18,7 +18,7 @@ - + diff --git a/creusot/tests/should_succeed/filter_positive/why3shapes.gz b/creusot/tests/should_succeed/filter_positive/why3shapes.gz index 878d0edfab..2b1ce3d1d1 100644 Binary files a/creusot/tests/should_succeed/filter_positive/why3shapes.gz and b/creusot/tests/should_succeed/filter_positive/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/hashmap/why3session.xml b/creusot/tests/should_succeed/hashmap/why3session.xml index f8ce4b4682..cbc6805254 100644 --- a/creusot/tests/should_succeed/hashmap/why3session.xml +++ b/creusot/tests/should_succeed/hashmap/why3session.xml @@ -2,98 +2,98 @@ + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -114,45 +114,45 @@ - + - + - + - + - + - + - + - + - + - + - + @@ -166,52 +166,52 @@ - + - + - + - + - + - + - + - + - + - + - + - + @@ -235,7 +235,7 @@ - + @@ -250,7 +250,7 @@ - + @@ -261,85 +261,85 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -348,124 +348,124 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -474,40 +474,40 @@ - + - + - + - + - + - + - + - + - + - + @@ -519,12 +519,12 @@ - + - + diff --git a/creusot/tests/should_succeed/hashmap/why3shapes.gz b/creusot/tests/should_succeed/hashmap/why3shapes.gz index 2c28e59a52..33e6ebb9e4 100644 Binary files a/creusot/tests/should_succeed/hashmap/why3shapes.gz and b/creusot/tests/should_succeed/hashmap/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/heapsort_generic/why3session.xml b/creusot/tests/should_succeed/heapsort_generic/why3session.xml index 01f99d27a7..75ae8d850f 100644 --- a/creusot/tests/should_succeed/heapsort_generic/why3session.xml +++ b/creusot/tests/should_succeed/heapsort_generic/why3session.xml @@ -2,173 +2,168 @@ - - + + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - + @@ -177,116 +172,28 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + @@ -295,150 +202,130 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz b/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz index a41b99bf4e..2b0cb82dd2 100644 Binary files a/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz and b/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/hillel/why3session.xml b/creusot/tests/should_succeed/hillel/why3session.xml index d10ed96f04..9a527d20be 100644 --- a/creusot/tests/should_succeed/hillel/why3session.xml +++ b/creusot/tests/should_succeed/hillel/why3session.xml @@ -5,130 +5,130 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -163,12 +163,12 @@ - + - + @@ -180,79 +180,79 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/index_range/why3session.xml b/creusot/tests/should_succeed/index_range/why3session.xml index 3857a39796..8de6b3ec0c 100644 --- a/creusot/tests/should_succeed/index_range/why3session.xml +++ b/creusot/tests/should_succeed/index_range/why3session.xml @@ -4,7 +4,7 @@ - + @@ -21,196 +21,196 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/index_range/why3shapes.gz b/creusot/tests/should_succeed/index_range/why3shapes.gz index 4f7f35d875..4037316888 100644 Binary files a/creusot/tests/should_succeed/index_range/why3shapes.gz and b/creusot/tests/should_succeed/index_range/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml b/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml index a72a1e213a..09fba0dd9e 100644 --- a/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml +++ b/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ite_normalize/why3session.xml b/creusot/tests/should_succeed/ite_normalize/why3session.xml index 2f1e4968c8..c9d201d4cc 100644 --- a/creusot/tests/should_succeed/ite_normalize/why3session.xml +++ b/creusot/tests/should_succeed/ite_normalize/why3session.xml @@ -2,19 +2,19 @@ - + - + - + @@ -24,7 +24,7 @@ - + @@ -34,12 +34,12 @@ - + - + @@ -49,12 +49,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ite_normalize/why3shapes.gz b/creusot/tests/should_succeed/ite_normalize/why3shapes.gz index ffe63ec443..2d3fef4460 100644 Binary files a/creusot/tests/should_succeed/ite_normalize/why3shapes.gz and b/creusot/tests/should_succeed/ite_normalize/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/01_range/why3session.xml b/creusot/tests/should_succeed/iterators/01_range/why3session.xml index 21451b408c..d1cf1b6803 100644 --- a/creusot/tests/should_succeed/iterators/01_range/why3session.xml +++ b/creusot/tests/should_succeed/iterators/01_range/why3session.xml @@ -2,43 +2,43 @@ - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml index e4cf9c256a..4514f8e5fe 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml +++ b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml @@ -2,14 +2,14 @@ + - - + @@ -39,7 +39,7 @@ - + @@ -50,19 +50,19 @@ - + - + - + @@ -74,53 +74,53 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml index 77bf4a6974..d29482b74f 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml +++ b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml @@ -2,195 +2,187 @@ - + - + - + - + - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - - - - - + diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz b/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz index 879ed20366..15da88baad 100644 Binary files a/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz and b/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml index 0c1f8d3819..7607b9d1ba 100644 --- a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml +++ b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml @@ -3,12 +3,12 @@ "https://www.why3.org/why3session.dtd"> - + - + @@ -27,13 +27,13 @@ - + - + - + diff --git a/creusot/tests/should_succeed/iterators/05_map/why3session.xml b/creusot/tests/should_succeed/iterators/05_map/why3session.xml index e10768d0fe..f0d47a7084 100644 --- a/creusot/tests/should_succeed/iterators/05_map/why3session.xml +++ b/creusot/tests/should_succeed/iterators/05_map/why3session.xml @@ -4,8 +4,8 @@ + - @@ -39,51 +39,51 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -111,7 +111,7 @@ - + @@ -130,7 +130,7 @@ - + @@ -141,58 +141,58 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index 53cb19a983..e85a9c10a7 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -2,7 +2,7 @@ - + @@ -39,25 +39,25 @@ - + - + - + - + - + @@ -66,25 +66,25 @@ - + - + - + - + - + - + - + @@ -93,7 +93,7 @@ - + @@ -108,7 +108,7 @@ - + @@ -139,31 +139,31 @@ - + - + - + - + - + @@ -174,44 +174,44 @@ - + - + - + - + - + - + - + - + @@ -220,7 +220,7 @@ - + @@ -262,7 +262,7 @@ - + @@ -273,10 +273,10 @@ - + - + @@ -285,37 +285,37 @@ - + - + - + - + - + - + - + - + - + @@ -327,39 +327,39 @@ - + - + - + - + - + - + - + - + - + @@ -369,23 +369,23 @@ - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml index a8bfaf6eef..cd00a5fde8 100644 --- a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml +++ b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml @@ -2,18 +2,18 @@ - + - + - + @@ -39,23 +39,23 @@ - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml b/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml index 106d904224..bec73e2458 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml +++ b/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml @@ -2,83 +2,83 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -87,79 +87,79 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz index 0ad26e67a4..588b9de059 100644 Binary files a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz and b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml index 6401fbd274..5b47fe0c27 100644 --- a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml +++ b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/10_once/why3session.xml b/creusot/tests/should_succeed/iterators/10_once/why3session.xml index b93a7b390a..1fcf8a0f82 100644 --- a/creusot/tests/should_succeed/iterators/10_once/why3session.xml +++ b/creusot/tests/should_succeed/iterators/10_once/why3session.xml @@ -2,37 +2,37 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml index 6b6921b368..2c3fe62c76 100644 --- a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml +++ b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/12_zip/why3session.xml b/creusot/tests/should_succeed/iterators/12_zip/why3session.xml index f01aca7c3b..3900dcd36e 100644 --- a/creusot/tests/should_succeed/iterators/12_zip/why3session.xml +++ b/creusot/tests/should_succeed/iterators/12_zip/why3session.xml @@ -2,13 +2,13 @@ + - - + @@ -31,25 +31,25 @@ - + - + - + - + - + - + - + @@ -79,12 +79,12 @@ - - - + + + diff --git a/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz b/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz index a4935dfd79..92404f6432 100644 Binary files a/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz and b/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml index e31fb4ea76..187ede3955 100644 --- a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml +++ b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml index ad84849a1f..a44e6fe54a 100644 --- a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml +++ b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - - - - + - + + + + diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz b/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz index dd930c6d47..276dce2ff8 100644 Binary files a/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz and b/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml b/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml index 9fb8519e9b..6de1129525 100644 --- a/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml +++ b/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml @@ -3,66 +3,66 @@ "https://www.why3.org/why3session.dtd"> - + - + - + - + - + - + - + - + - + - + - + - + - - - - + + + + - + diff --git a/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz b/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz index 980e4e9bfb..d517ba9025 100644 Binary files a/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz and b/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/16_take/why3session.xml b/creusot/tests/should_succeed/iterators/16_take/why3session.xml index 5c62559519..1ed030a11e 100644 --- a/creusot/tests/should_succeed/iterators/16_take/why3session.xml +++ b/creusot/tests/should_succeed/iterators/16_take/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/knapsack/why3session.xml b/creusot/tests/should_succeed/knapsack/why3session.xml index 35af7bc97c..d21c1dd489 100644 --- a/creusot/tests/should_succeed/knapsack/why3session.xml +++ b/creusot/tests/should_succeed/knapsack/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,299 +13,299 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/knapsack/why3shapes.gz b/creusot/tests/should_succeed/knapsack/why3shapes.gz index 86b2531a68..4706370563 100644 Binary files a/creusot/tests/should_succeed/knapsack/why3shapes.gz and b/creusot/tests/should_succeed/knapsack/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/knapsack_full/why3session.xml b/creusot/tests/should_succeed/knapsack_full/why3session.xml index c07fb1345f..596cc98e5b 100644 --- a/creusot/tests/should_succeed/knapsack_full/why3session.xml +++ b/creusot/tests/should_succeed/knapsack_full/why3session.xml @@ -4,8 +4,7 @@ - - + @@ -20,12 +19,12 @@ - + - + @@ -37,344 +36,340 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - + diff --git a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz index c622b5b72b..6a253a4d73 100644 Binary files a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz and b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/lang/assoc_type/why3session.xml b/creusot/tests/should_succeed/lang/assoc_type/why3session.xml index 0b2605d480..8fdf9d5475 100644 --- a/creusot/tests/should_succeed/lang/assoc_type/why3session.xml +++ b/creusot/tests/should_succeed/lang/assoc_type/why3session.xml @@ -2,27 +2,12 @@ - + - - - - - - - - - - - - - - - - + diff --git a/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz b/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz index c47a7dc23a..1241315588 100644 Binary files a/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz and b/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/lang/modules/why3session.xml b/creusot/tests/should_succeed/lang/modules/why3session.xml index d4edf9a301..4bb5718eeb 100644 --- a/creusot/tests/should_succeed/lang/modules/why3session.xml +++ b/creusot/tests/should_succeed/lang/modules/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/lang/unary_op/why3session.xml b/creusot/tests/should_succeed/lang/unary_op/why3session.xml index 0c082c6da0..2730a6abbe 100644 --- a/creusot/tests/should_succeed/lang/unary_op/why3session.xml +++ b/creusot/tests/should_succeed/lang/unary_op/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/lang/while_let/why3session.xml b/creusot/tests/should_succeed/lang/while_let/why3session.xml index 32a8f03c27..26f83345d2 100644 --- a/creusot/tests/should_succeed/lang/while_let/why3session.xml +++ b/creusot/tests/should_succeed/lang/while_let/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/list_index_mut/why3session.xml b/creusot/tests/should_succeed/list_index_mut/why3session.xml index a7d03fcecf..c399061f15 100644 --- a/creusot/tests/should_succeed/list_index_mut/why3session.xml +++ b/creusot/tests/should_succeed/list_index_mut/why3session.xml @@ -2,22 +2,22 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/list_index_mut/why3shapes.gz b/creusot/tests/should_succeed/list_index_mut/why3shapes.gz index 623415d584..5ab029a37b 100644 Binary files a/creusot/tests/should_succeed/list_index_mut/why3shapes.gz and b/creusot/tests/should_succeed/list_index_mut/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml index 7b69c31810..f449ab1708 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml +++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml @@ -4,8 +4,8 @@ + - @@ -36,22 +36,22 @@ - + - + - + - + - + @@ -63,16 +63,16 @@ - + - + - + - + @@ -81,7 +81,7 @@ - + @@ -102,7 +102,7 @@ - + @@ -124,7 +124,7 @@ - + @@ -149,7 +149,7 @@ - + @@ -164,22 +164,22 @@ - + - + - + - + - + @@ -187,32 +187,32 @@ - + - + - + - + - + - + - + @@ -221,10 +221,10 @@ - + - + @@ -252,7 +252,7 @@ - + @@ -260,7 +260,7 @@ - + @@ -271,10 +271,10 @@ - + - + @@ -288,14 +288,14 @@ - + - + @@ -304,19 +304,19 @@ - + - + - + - + - + @@ -326,7 +326,7 @@ - + @@ -335,10 +335,10 @@ - + - + @@ -347,38 +347,38 @@ - + - + - + - + - + - + - + - + - + @@ -391,16 +391,16 @@ - + - + - + @@ -411,24 +411,24 @@ - + - + - + - + @@ -439,16 +439,16 @@ - + - + - + @@ -463,7 +463,7 @@ - + @@ -472,10 +472,10 @@ - + - + @@ -484,7 +484,7 @@ - + @@ -498,7 +498,7 @@ - + @@ -507,10 +507,10 @@ - + - + @@ -523,14 +523,14 @@ - + - + @@ -541,13 +541,13 @@ - + - + @@ -575,41 +575,41 @@ - + - + - + - + - + - + - + - + - + - + @@ -619,16 +619,16 @@ - + - + - + - + @@ -637,16 +637,16 @@ - + - + - + - + @@ -670,12 +670,12 @@ - + - + diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz index f2d31128a0..ba5fad77ff 100644 Binary files a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz and b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/mapping_test/why3session.xml b/creusot/tests/should_succeed/mapping_test/why3session.xml index 9b502930ef..55c7912090 100644 --- a/creusot/tests/should_succeed/mapping_test/why3session.xml +++ b/creusot/tests/should_succeed/mapping_test/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/mapping_test/why3shapes.gz b/creusot/tests/should_succeed/mapping_test/why3shapes.gz index 786b759a62..47c7dd3945 100644 Binary files a/creusot/tests/should_succeed/mapping_test/why3shapes.gz and b/creusot/tests/should_succeed/mapping_test/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/match_int/why3session.xml b/creusot/tests/should_succeed/match_int/why3session.xml index fdb1011fce..b71f0515f5 100644 --- a/creusot/tests/should_succeed/match_int/why3session.xml +++ b/creusot/tests/should_succeed/match_int/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/mc91/why3session.xml b/creusot/tests/should_succeed/mc91/why3session.xml index 55e9bbc6ef..688984f7fd 100644 --- a/creusot/tests/should_succeed/mc91/why3session.xml +++ b/creusot/tests/should_succeed/mc91/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/mutex/why3session.xml b/creusot/tests/should_succeed/mutex/why3session.xml index d9bbafeff6..6ff99c5a55 100644 --- a/creusot/tests/should_succeed/mutex/why3session.xml +++ b/creusot/tests/should_succeed/mutex/why3session.xml @@ -4,7 +4,7 @@ - + @@ -14,7 +14,7 @@ - + diff --git a/creusot/tests/should_succeed/ord_trait/why3session.xml b/creusot/tests/should_succeed/ord_trait/why3session.xml index 656138d2a9..0f065d1c99 100644 --- a/creusot/tests/should_succeed/ord_trait/why3session.xml +++ b/creusot/tests/should_succeed/ord_trait/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,12 +13,12 @@ - + - + diff --git a/creusot/tests/should_succeed/projection_toggle/why3session.xml b/creusot/tests/should_succeed/projection_toggle/why3session.xml index b9ad1d6cc7..8d524bf7d8 100644 --- a/creusot/tests/should_succeed/projection_toggle/why3session.xml +++ b/creusot/tests/should_succeed/projection_toggle/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/red_black_tree/why3session.xml b/creusot/tests/should_succeed/red_black_tree/why3session.xml index 1518d4eb5d..a783d468d1 100644 --- a/creusot/tests/should_succeed/red_black_tree/why3session.xml +++ b/creusot/tests/should_succeed/red_black_tree/why3session.xml @@ -3,14 +3,14 @@ "https://www.why3.org/why3session.dtd"> + - - + @@ -20,22 +20,22 @@ - + - + - + - + @@ -49,80 +49,80 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -134,13 +134,13 @@ - + - + - + @@ -152,58 +152,58 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -218,10 +218,10 @@ - + - + @@ -230,19 +230,19 @@ - + - + - + - + - + @@ -251,16 +251,16 @@ - + - + - + - + @@ -287,90 +287,90 @@ - + - + + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -386,7 +386,7 @@ - + @@ -398,12 +398,12 @@ - + - + @@ -418,7 +418,7 @@ - + @@ -429,12 +429,12 @@ - + - + @@ -443,17 +443,17 @@ - + - + - + @@ -462,33 +462,33 @@ - + - + - + - + - + - + - + @@ -511,26 +511,26 @@ - + - + - + - + @@ -550,19 +550,19 @@ - + - + - + @@ -583,7 +583,7 @@ - + @@ -592,7 +592,7 @@ - + @@ -601,17 +601,17 @@ - + - + - + @@ -620,7 +620,7 @@ - + @@ -633,7 +633,7 @@ - + @@ -644,7 +644,7 @@ - + @@ -655,30 +655,30 @@ - + - + - + - + - + - + @@ -690,7 +690,7 @@ - + @@ -699,7 +699,7 @@ - + @@ -710,13 +710,13 @@ - + - + - + @@ -731,7 +731,7 @@ - + @@ -744,7 +744,7 @@ - + @@ -755,7 +755,7 @@ - + @@ -766,27 +766,27 @@ - + - + - + - + - + @@ -801,7 +801,7 @@ - + @@ -814,7 +814,7 @@ - + @@ -832,33 +832,33 @@ - + - + - + - + - + - + - + @@ -867,7 +867,7 @@ - + @@ -890,7 +890,7 @@ - + @@ -906,7 +906,7 @@ - + @@ -915,24 +915,24 @@ - + - + - + - + @@ -951,17 +951,17 @@ - + - + - + @@ -972,24 +972,24 @@ - + - + - + - + @@ -1002,21 +1002,21 @@ - + - + - + @@ -1037,22 +1037,22 @@ - + - + - + - + - + @@ -1061,13 +1061,13 @@ - + - + - + @@ -1101,13 +1101,13 @@ - + - + - + @@ -1116,10 +1116,10 @@ - + - + @@ -1338,7 +1338,7 @@ - + @@ -1350,25 +1350,25 @@ - + - + - + - + @@ -1377,10 +1377,10 @@ - + - + @@ -1389,22 +1389,22 @@ - + - + - + - + - + @@ -1569,84 +1569,84 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1667,25 +1667,25 @@ - + - + - + - + - + - + @@ -1736,7 +1736,7 @@ - + @@ -1759,37 +1759,37 @@ - + - + - + - + - + - + - + - + - + - + - + @@ -1810,25 +1810,25 @@ - + - + - + - + - + - + @@ -1843,7 +1843,7 @@ - + @@ -1852,44 +1852,48 @@ - + - + - + - + - + - + - + + + + + - + - + - + - + @@ -1912,7 +1916,7 @@ - + @@ -1937,7 +1941,7 @@ - + @@ -1947,7 +1951,7 @@ - + @@ -1957,7 +1961,7 @@ - + @@ -1965,7 +1969,7 @@ - + @@ -1988,7 +1992,7 @@ - + @@ -2152,7 +2156,7 @@ - + @@ -2226,7 +2230,7 @@ - + @@ -2321,16 +2325,16 @@ - + - + - + @@ -2339,13 +2343,13 @@ - + - + @@ -2357,28 +2361,28 @@ - + - + - + - + - + - + @@ -2386,24 +2390,24 @@ - + - + - + - + @@ -2415,7 +2419,7 @@ - + @@ -2428,15 +2432,15 @@ - + - + - + @@ -2448,7 +2452,7 @@ - + @@ -2463,19 +2467,19 @@ - + - + - + - + @@ -2484,7 +2488,7 @@ - + @@ -2493,21 +2497,25 @@ - + - + - + - + - + + + + + @@ -2515,10 +2523,10 @@ - + - + @@ -2534,7 +2542,7 @@ - + @@ -2551,7 +2559,7 @@ - + @@ -2560,13 +2568,13 @@ - + - + - + @@ -2625,7 +2633,7 @@ - + @@ -2733,7 +2741,7 @@ - + @@ -2766,7 +2774,7 @@ - + @@ -2775,13 +2783,13 @@ - + - + - + @@ -2793,7 +2801,7 @@ - + @@ -2805,10 +2813,10 @@ - + - + @@ -2817,10 +2825,10 @@ - + - + @@ -2872,7 +2880,7 @@ - + @@ -2894,7 +2902,7 @@ - + @@ -2920,7 +2928,7 @@ - + @@ -2933,7 +2941,7 @@ - + @@ -2941,7 +2949,7 @@ - + @@ -2956,7 +2964,7 @@ - + @@ -2965,62 +2973,66 @@ - + - + - + - + - + - + - + - + - + + + + + - + - + - + - + @@ -3032,25 +3044,25 @@ - + - + - + - + - + @@ -3059,21 +3071,25 @@ - + - + - + - + - + + + + + @@ -3084,52 +3100,52 @@ - + - + - + - + - + - + - + - + - + - + - + @@ -3149,10 +3165,10 @@ - + - + @@ -3160,7 +3176,7 @@ - + @@ -3172,10 +3188,10 @@ - + - + @@ -3191,43 +3207,43 @@ - + - + - + - + - + - + - + - + - + - + @@ -3269,7 +3285,7 @@ - + @@ -3345,14 +3361,14 @@ - + - + @@ -3366,12 +3382,12 @@ - + - + @@ -3395,7 +3411,7 @@ - + @@ -3404,7 +3420,7 @@ - + @@ -3414,17 +3430,17 @@ - + - + - + @@ -3439,7 +3455,7 @@ - + @@ -3492,7 +3508,7 @@ - + @@ -3532,10 +3548,10 @@ - + - + @@ -3560,7 +3576,7 @@ - + @@ -3585,7 +3601,7 @@ - + @@ -3604,7 +3620,7 @@ - + @@ -3630,7 +3646,7 @@ - + @@ -3688,10 +3704,10 @@ - + - + @@ -3742,7 +3758,7 @@ - + @@ -3763,7 +3779,7 @@ - + @@ -3923,14 +3939,18 @@ - + - + + + + + @@ -3992,7 +4012,7 @@ - + @@ -4001,7 +4021,7 @@ - + @@ -4065,12 +4085,12 @@ - + - + @@ -4086,7 +4106,7 @@ - + @@ -4113,34 +4133,34 @@ - + - + - + - + - + - + - + - + @@ -4149,31 +4169,31 @@ - + - + - + - + - + - + @@ -4294,7 +4314,7 @@ - + @@ -4307,96 +4327,96 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -4420,7 +4440,7 @@ - + @@ -4445,7 +4465,7 @@ - + @@ -4453,7 +4473,18 @@ - + + + + + + + + + + + + @@ -4464,7 +4495,7 @@ - + @@ -4478,12 +4509,12 @@ - + - + @@ -4492,7 +4523,7 @@ - + @@ -4505,14 +4536,14 @@ - + - + diff --git a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz index fe554d1320..ca8a8e6cfc 100644 Binary files a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz and b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/resolve_uninit/why3session.xml b/creusot/tests/should_succeed/resolve_uninit/why3session.xml index 84f5e9d973..37bc54b759 100644 --- a/creusot/tests/should_succeed/resolve_uninit/why3session.xml +++ b/creusot/tests/should_succeed/resolve_uninit/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml index d1ad93ed1a..09a60aee0f 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml index 83d3114756..5ee3e60ea8 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml @@ -2,13 +2,13 @@ + - - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml index 9a95523da0..cee264aafe 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml @@ -3,12 +3,12 @@ "https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml index 000f1a83fd..b8ea06b529 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml @@ -2,13 +2,13 @@ + - - + @@ -18,7 +18,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz index 72e8ec813a..87d5b058d0 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml index ff2a97b0eb..65cf44a38f 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml @@ -2,13 +2,13 @@ + - - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz index 61064af20e..74bfe9d32c 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml index afc9d52bcc..9349f090d3 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml @@ -2,13 +2,13 @@ - + - + @@ -18,12 +18,12 @@ - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz index 30f95ddefb..2c28d6e656 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml index 13138a09eb..59a106f903 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml @@ -2,13 +2,13 @@ - + - + @@ -23,7 +23,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz index aaa9e12f0e..8b808c13e7 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/selection_sort_generic/why3session.xml b/creusot/tests/should_succeed/selection_sort_generic/why3session.xml index 28c6265065..88ff4a6f9a 100644 --- a/creusot/tests/should_succeed/selection_sort_generic/why3session.xml +++ b/creusot/tests/should_succeed/selection_sort_generic/why3session.xml @@ -5,99 +5,99 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -117,14 +117,14 @@ - + - + @@ -142,37 +142,37 @@ - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz b/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz index 17febaf113..08af88e0eb 100644 Binary files a/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz and b/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/slices/01/why3session.xml b/creusot/tests/should_succeed/slices/01/why3session.xml index c13a3cf1fb..0a925bd1eb 100644 --- a/creusot/tests/should_succeed/slices/01/why3session.xml +++ b/creusot/tests/should_succeed/slices/01/why3session.xml @@ -2,8 +2,8 @@ + - @@ -13,12 +13,12 @@ - + - + diff --git a/creusot/tests/should_succeed/slices/01/why3shapes.gz b/creusot/tests/should_succeed/slices/01/why3shapes.gz index 88d5b3d077..7cc3046962 100644 Binary files a/creusot/tests/should_succeed/slices/01/why3shapes.gz and b/creusot/tests/should_succeed/slices/01/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/slices/02_std/why3session.xml b/creusot/tests/should_succeed/slices/02_std/why3session.xml index 40bc751b65..7af9d8b48d 100644 --- a/creusot/tests/should_succeed/slices/02_std/why3session.xml +++ b/creusot/tests/should_succeed/slices/02_std/why3session.xml @@ -2,36 +2,36 @@ - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz index 45dd894c5a..8466df0f3c 100644 Binary files a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz and b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/sparse_array/why3session.xml b/creusot/tests/should_succeed/sparse_array/why3session.xml index 829e100b4c..186aa7a2f0 100644 --- a/creusot/tests/should_succeed/sparse_array/why3session.xml +++ b/creusot/tests/should_succeed/sparse_array/why3session.xml @@ -3,8 +3,8 @@ "https://www.why3.org/why3session.dtd"> + - @@ -29,14 +29,14 @@ - + + - @@ -59,8 +59,8 @@ + - @@ -70,27 +70,27 @@ + - + - + - - + + - + - @@ -103,8 +103,8 @@ + - @@ -114,16 +114,16 @@ + - + - @@ -158,7 +158,7 @@ - + diff --git a/creusot/tests/should_succeed/specification/division/why3session.xml b/creusot/tests/should_succeed/specification/division/why3session.xml index 9831977079..a285ee6e90 100644 --- a/creusot/tests/should_succeed/specification/division/why3session.xml +++ b/creusot/tests/should_succeed/specification/division/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/specification/forall/why3session.xml b/creusot/tests/should_succeed/specification/forall/why3session.xml index 7bd4f2e982..6016c0bfd1 100644 --- a/creusot/tests/should_succeed/specification/forall/why3session.xml +++ b/creusot/tests/should_succeed/specification/forall/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/specification/logic_call/why3session.xml b/creusot/tests/should_succeed/specification/logic_call/why3session.xml index 042d7a20af..2de1bd8a52 100644 --- a/creusot/tests/should_succeed/specification/logic_call/why3session.xml +++ b/creusot/tests/should_succeed/specification/logic_call/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/specification/logic_functions/why3session.xml b/creusot/tests/should_succeed/specification/logic_functions/why3session.xml index f169c0e85a..8784a59d64 100644 --- a/creusot/tests/should_succeed/specification/logic_functions/why3session.xml +++ b/creusot/tests/should_succeed/specification/logic_functions/why3session.xml @@ -1,18 +1,18 @@ +"https://www.why3.org/why3session.dtd"> - + - + - + diff --git a/creusot/tests/should_succeed/specification/model/why3session.xml b/creusot/tests/should_succeed/specification/model/why3session.xml index 2670a9f805..6946305c39 100644 --- a/creusot/tests/should_succeed/specification/model/why3session.xml +++ b/creusot/tests/should_succeed/specification/model/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> diff --git a/creusot/tests/should_succeed/specification/trusted/why3session.xml b/creusot/tests/should_succeed/specification/trusted/why3session.xml index 59232d8a9d..a96906a2ce 100644 --- a/creusot/tests/should_succeed/specification/trusted/why3session.xml +++ b/creusot/tests/should_succeed/specification/trusted/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/sum/why3session.xml b/creusot/tests/should_succeed/sum/why3session.xml index c8a4da0916..ce8b5a03bd 100644 --- a/creusot/tests/should_succeed/sum/why3session.xml +++ b/creusot/tests/should_succeed/sum/why3session.xml @@ -5,38 +5,38 @@ - + - + - + - + - + - + - + - + @@ -45,7 +45,7 @@ - + @@ -69,10 +69,10 @@ - + - + diff --git a/creusot/tests/should_succeed/sum_of_odds/why3session.xml b/creusot/tests/should_succeed/sum_of_odds/why3session.xml index af019f2ad0..2547fabc9f 100644 --- a/creusot/tests/should_succeed/sum_of_odds/why3session.xml +++ b/creusot/tests/should_succeed/sum_of_odds/why3session.xml @@ -3,12 +3,12 @@ "https://www.why3.org/why3session.dtd"> - + - + @@ -20,53 +20,53 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/swap_borrows/why3session.xml b/creusot/tests/should_succeed/swap_borrows/why3session.xml index 59893a90fe..61a81227d6 100644 --- a/creusot/tests/should_succeed/swap_borrows/why3session.xml +++ b/creusot/tests/should_succeed/swap_borrows/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/syntax/02_operators/why3session.xml b/creusot/tests/should_succeed/syntax/02_operators/why3session.xml index d427ef5464..de849f629a 100644 --- a/creusot/tests/should_succeed/syntax/02_operators/why3session.xml +++ b/creusot/tests/should_succeed/syntax/02_operators/why3session.xml @@ -2,29 +2,29 @@ + - - + - + - + - + @@ -39,7 +39,7 @@ - + @@ -49,12 +49,12 @@ - + - + diff --git a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml index 5e4ccbb6e1..c881ea4ac3 100644 --- a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml +++ b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,12 +13,12 @@ - + - + diff --git a/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml b/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml index e632af90a0..67b38281b1 100644 --- a/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml +++ b/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml @@ -3,8 +3,8 @@ "https://www.why3.org/why3session.dtd"> + - @@ -14,7 +14,7 @@ - + @@ -24,12 +24,12 @@ - + - + diff --git a/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml b/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml index dd4d2d99d3..aec4634d3c 100644 --- a/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml +++ b/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml b/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml index 230f2dd9d4..5d8c15e124 100644 --- a/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml +++ b/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml @@ -3,7 +3,7 @@ "https://www.why3.org/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz b/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz index ee4613588c..a05dde6e2d 100644 Binary files a/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz and b/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml b/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml index 65273d8982..1545b0f4e2 100644 --- a/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml +++ b/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz b/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz index a8176c822f..7ca824d7c6 100644 Binary files a/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz and b/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml b/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml index efe335d229..0a8f0e52b1 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml +++ b/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml @@ -3,17 +3,17 @@ "https://www.why3.org/why3session.dtd"> - + - + - + @@ -23,12 +23,12 @@ - + - + @@ -38,12 +38,12 @@ - + - + diff --git a/creusot/tests/should_succeed/traits/02/why3session.xml b/creusot/tests/should_succeed/traits/02/why3session.xml index 69068c8ae1..bfaf943cf4 100644 --- a/creusot/tests/should_succeed/traits/02/why3session.xml +++ b/creusot/tests/should_succeed/traits/02/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/traits/12_default_method/why3session.xml b/creusot/tests/should_succeed/traits/12_default_method/why3session.xml index 51bfbed3f7..b3de5863b8 100644 --- a/creusot/tests/should_succeed/traits/12_default_method/why3session.xml +++ b/creusot/tests/should_succeed/traits/12_default_method/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml b/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml index 0116e01978..6a19a9c4d4 100644 --- a/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml +++ b/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml @@ -1,18 +1,18 @@ +"https://www.why3.org/why3session.dtd"> - + - + - + diff --git a/creusot/tests/should_succeed/traits/15_impl_interfaces/why3session.xml b/creusot/tests/should_succeed/traits/15_impl_interfaces/why3session.xml index 06ff9d1f3f..7a39e3caec 100644 --- a/creusot/tests/should_succeed/traits/15_impl_interfaces/why3session.xml +++ b/creusot/tests/should_succeed/traits/15_impl_interfaces/why3session.xml @@ -1,6 +1,6 @@ +"https://www.why3.org/why3session.dtd"> diff --git a/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml b/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml index 1874f4a3d9..3bee6003af 100644 --- a/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml +++ b/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml b/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml index 72a1d23385..666fcc54b4 100644 --- a/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml +++ b/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml @@ -3,12 +3,12 @@ "https://www.why3.org/why3session.dtd"> - + - + @@ -18,12 +18,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/generated/why3session.xml b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml index 188270fc8c..1385780d1d 100644 --- a/creusot/tests/should_succeed/type_invariants/generated/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml b/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml index cce66003e4..ca555adf5d 100644 --- a/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml @@ -3,17 +3,17 @@ "https://www.why3.org/why3session.dtd"> - + - + - + @@ -23,7 +23,7 @@ - + diff --git a/creusot/tests/should_succeed/type_invariants/quant/why3session.xml b/creusot/tests/should_succeed/type_invariants/quant/why3session.xml index 9a4cbfb0ea..50f31557fb 100644 --- a/creusot/tests/should_succeed/type_invariants/quant/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/quant/why3session.xml @@ -2,17 +2,17 @@ + - - - + + - + diff --git a/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml b/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml index 9882af733f..910a91ba6d 100644 --- a/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml @@ -1,13 +1,13 @@ +"https://www.why3.org/why3session.dtd"> - + - + diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml b/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml index 73afbe3817..70dd01040b 100644 --- a/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz b/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz index 98e5159798..d75fca7e50 100644 Binary files a/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz and b/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/unnest/why3session.xml b/creusot/tests/should_succeed/unnest/why3session.xml index d8b4636f05..348c0049ed 100644 --- a/creusot/tests/should_succeed/unnest/why3session.xml +++ b/creusot/tests/should_succeed/unnest/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/unused_in_loop/why3session.xml b/creusot/tests/should_succeed/unused_in_loop/why3session.xml index 967881282a..4bda28e445 100644 --- a/creusot/tests/should_succeed/unused_in_loop/why3session.xml +++ b/creusot/tests/should_succeed/unused_in_loop/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vecdeque/why3session.xml b/creusot/tests/should_succeed/vecdeque/why3session.xml index b14bbbe157..9351d55684 100644 --- a/creusot/tests/should_succeed/vecdeque/why3session.xml +++ b/creusot/tests/should_succeed/vecdeque/why3session.xml @@ -3,137 +3,137 @@ "https://www.why3.org/why3session.dtd"> - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vecdeque/why3shapes.gz b/creusot/tests/should_succeed/vecdeque/why3shapes.gz index f3332fdeaf..af6312643c 100644 Binary files a/creusot/tests/should_succeed/vecdeque/why3shapes.gz and b/creusot/tests/should_succeed/vecdeque/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml index 326a99d456..b0c6be8595 100644 --- a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml +++ b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml @@ -5,7 +5,7 @@ - + @@ -15,79 +15,79 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -95,7 +95,7 @@ - + diff --git a/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz b/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz index f9c9c00c41..dd5e825198 100644 Binary files a/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz and b/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz index 57292663de..cd01dab9bb 100644 Binary files a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz and b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz b/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz index 2ed60b930f..6a58ab21a1 100644 Binary files a/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz and b/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml index 920b26633f..0d73af9dcf 100644 --- a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml +++ b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml @@ -3,15 +3,15 @@ "https://www.why3.org/why3session.dtd"> + - - + @@ -23,76 +23,76 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -104,13 +104,13 @@ - + - + - + diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz index 18d18835cf..24a554d250 100644 Binary files a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz and b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml b/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml index e9cfe8778a..168bba6e0d 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml +++ b/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml @@ -2,87 +2,87 @@ + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -95,7 +95,7 @@ - + @@ -110,7 +110,7 @@ - + @@ -133,7 +133,7 @@ - + @@ -148,7 +148,7 @@ - + @@ -161,25 +161,25 @@ - + - + - + - + - + @@ -188,7 +188,7 @@ - + @@ -197,25 +197,25 @@ - + - + - + - + - + - + - + @@ -227,7 +227,7 @@ - + @@ -240,10 +240,10 @@ - + - + @@ -260,97 +260,97 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -359,12 +359,12 @@ - + - + @@ -379,7 +379,7 @@ - + @@ -394,7 +394,7 @@ - + @@ -417,7 +417,7 @@ - + @@ -432,7 +432,7 @@ - + @@ -445,22 +445,22 @@ - + - + - + - + - + - + @@ -473,7 +473,7 @@ - + diff --git a/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz b/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz index 19a30b6d89..b7b57125a0 100644 Binary files a/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz and b/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/07_read_write/why3session.xml b/creusot/tests/should_succeed/vector/07_read_write/why3session.xml index 2d10346b52..1ec500823c 100644 --- a/creusot/tests/should_succeed/vector/07_read_write/why3session.xml +++ b/creusot/tests/should_succeed/vector/07_read_write/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz b/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz index bfe8b45a8f..b14f9e9911 100644 Binary files a/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz and b/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml index 437da35f86..b7f60b5c8a 100644 --- a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml +++ b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml @@ -4,8 +4,8 @@ + - @@ -18,25 +18,25 @@ - + - + - + - + - + - + - + @@ -45,10 +45,10 @@ - + - + @@ -57,31 +57,31 @@ - + - + - + - + - + - + @@ -93,7 +93,7 @@ - + diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz index 0e0a6e2749..84aa8139d4 100644 Binary files a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz and b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/09_capacity/why3session.xml b/creusot/tests/should_succeed/vector/09_capacity/why3session.xml index 176fd12722..ca8db80b45 100644 --- a/creusot/tests/should_succeed/vector/09_capacity/why3session.xml +++ b/creusot/tests/should_succeed/vector/09_capacity/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/testsuite_upgrade_prover b/testsuite_upgrade_prover new file mode 100755 index 0000000000..a34b943c5d --- /dev/null +++ b/testsuite_upgrade_prover @@ -0,0 +1,38 @@ +#!/bin/bash + +if [ -z "$1" ]; then + echo "Usage: $0 [path/to/test.mlcfg]" + echo "UPGRADE should be of the form: Alt-Ergo,2.4.3=Alt-Ergo,2.5.3" + echo "If no path to a specific mlcfg file is passed, tries to upgrade all tests in the testsuite" + echo "If a path to a mlcfg file is passed, tries to upgrade this test, and save the result even if it is a partial upgrade" + exit 1 +fi + +eval $(cargo run --bin dev-env) + +if [ -z "$2" ]; then + # upgrade all + failed=() + + shopt -s globstar + for file in creusot/tests/**/*.mlcfg; do + # only try to upgrade if it looks like there is a session directory + SESSION_DIR="$(dirname $file)/$(basename $file .mlcfg)" + if [ -d "$SESSION_DIR" ]; then + echo "==> Upgrading $file" + why3_tools upgrade -L./prelude --upgrade=$1 "$file" + if [ $? != 0 ]; then + failed+=("$file") + fi + fi + done + if [ ${#failed[@]} != 0 ]; then + echo "" + echo "Failed to upgrade the following tests:" + printf "%s\n" "${failed[@]}" + fi +else + # upgrade a specific test + echo "==> Upgrading $2" + why3_tools upgrade --allow-partial -L./prelude --upgrade=$1 "$2" +fi