From 8fb66272bb96a31987f32e46de351c44b8be57f5 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 12 Nov 2024 15:06:03 +0100 Subject: [PATCH] Update tests --- creusot/tests/should_fail/cycle.stderr | 20 ++++----- .../should_fail/ghost/non_terminating.stderr | 20 ++++----- .../complicated_traits_recursion.stderr | 18 +++----- .../terminates/mutual_recursion.stderr | 20 ++++----- .../terminates/mutual_recursion_trait.stderr | 20 ++++----- .../recursion_through_contract.stderr | 40 +++++++++--------- .../call_in_contract/why3session.xml | 14 ++++++ .../call_in_contract/why3shapes.gz | Bin 0 -> 105 bytes .../termination/default_impl/why3session.xml | 8 ++++ .../termination/default_impl/why3shapes.gz | Bin 0 -> 45 bytes .../default_impl_in_trait/why3session.xml | 8 ++++ .../default_impl_in_trait/why3shapes.gz | Bin 0 -> 45 bytes 12 files changed, 95 insertions(+), 73 deletions(-) create mode 100644 creusot/tests/should_succeed/termination/call_in_contract/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz create mode 100644 creusot/tests/should_succeed/termination/default_impl/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/default_impl/why3shapes.gz create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz diff --git a/creusot/tests/should_fail/cycle.stderr b/creusot/tests/should_fail/cycle.stderr index cdc6ee11ae..9a066437f3 100644 --- a/creusot/tests/should_fail/cycle.stderr +++ b/creusot/tests/should_fail/cycle.stderr @@ -1,19 +1,19 @@ -error: Mutually recursive functions: when calling `g`... - --> cycle.rs:12:1 +error: Mutually recursive functions: when calling `f`... + --> cycle.rs:6:1 | -12 | pub fn g(x: bool) { - | ^^^^^^^^^^^^^^^^^ +6 | pub fn f() { + | ^^^^^^^^^^ | -note: then `g` calls `f`... - --> cycle.rs:14:9 - | -14 | f(); - | ^^^ -note: finally `f` calls `g`. +note: then `f` calls `g`... --> cycle.rs:7:5 | 7 | g(true); | ^^^^^^^ +note: finally `g` calls `f`. + --> cycle.rs:14:9 + | +14 | f(); + | ^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/ghost/non_terminating.stderr b/creusot/tests/should_fail/ghost/non_terminating.stderr index 068db4028b..a31f2b69fa 100644 --- a/creusot/tests/should_fail/ghost/non_terminating.stderr +++ b/creusot/tests/should_fail/ghost/non_terminating.stderr @@ -27,22 +27,22 @@ note: looping occurs here | ^^^^^^^ = note: this error originates in the macro `ghost` (in Nightly builds, run with -Z macro-backtrace for more info) -error: Mutually recursive functions: when calling `f`... - --> non_terminating.rs:13:1 +error: Mutually recursive functions: when calling `recursive`... + --> non_terminating.rs:5:1 | -13 | fn f() { - | ^^^^^^ +5 | pub fn recursive() { + | ^^^^^^^^^^^^^^^^^^ | -note: then `f` calls `recursive`... - --> non_terminating.rs:14:5 - | -14 | recursive(); - | ^^^^^^^^^^^ -note: finally `recursive` calls `f`. +note: then `recursive` calls `f`... --> non_terminating.rs:7:9 | 7 | f(); | ^^^ +note: finally `f` calls `recursive`. + --> non_terminating.rs:14:5 + | +14 | recursive(); + | ^^^^^^^^^^^ error: aborting due to 2 previous errors; 1 warning emitted diff --git a/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr b/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr index bef6bfefea..7c53ccb0bf 100644 --- a/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr +++ b/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr @@ -1,18 +1,10 @@ -error: Mutually recursive functions: when calling `bar`... - --> complicated_traits_recursion.rs:18:1 +error: Mutually recursive functions: when calling `::foo`... + --> complicated_traits_recursion.rs:12:5 | -18 | / fn bar(_: I) -19 | | where -20 | | I: Iterator, -21 | | I::Item: Foo, - | |_________________^ +12 | fn foo() { + | ^^^^^^^^ | -note: then `bar` calls `::foo`... - --> complicated_traits_recursion.rs:23:5 - | -23 | I::Item::foo() - | ^^^^^^^^^^^^^^ -note: finally `::foo` calls `bar`. +note: then `::foo` might call `::foo` via the call to `bar`. --> complicated_traits_recursion.rs:13:9 | 13 | bar::>(std::iter::once(1i32)); diff --git a/creusot/tests/should_fail/terminates/mutual_recursion.stderr b/creusot/tests/should_fail/terminates/mutual_recursion.stderr index 8ecf6c8920..46599986fb 100644 --- a/creusot/tests/should_fail/terminates/mutual_recursion.stderr +++ b/creusot/tests/should_fail/terminates/mutual_recursion.stderr @@ -1,24 +1,24 @@ -error: Mutually recursive functions: when calling `f3`... - --> mutual_recursion.rs:18:1 +error: Mutually recursive functions: when calling `m::f1`... + --> mutual_recursion.rs:7:5 | -18 | fn f3() { - | ^^^^^^^ +7 | pub fn f1() { + | ^^^^^^^^^^^ | -note: then `f3` calls `m::f1`... - --> mutual_recursion.rs:19:5 - | -19 | m::f1(); - | ^^^^^^^ note: then `m::f1` calls `f2`... --> mutual_recursion.rs:8:9 | 8 | super::f2(); | ^^^^^^^^^^^ -note: finally `f2` calls `f3`. +note: then `f2` calls `f3`... --> mutual_recursion.rs:14:5 | 14 | f3(); | ^^^^ +note: finally `f3` calls `m::f1`. + --> mutual_recursion.rs:19:5 + | +19 | m::f1(); + | ^^^^^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr b/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr index 7724627ac2..6c41fe4b88 100644 --- a/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr +++ b/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr @@ -1,19 +1,19 @@ -error: Mutually recursive functions: when calling `bar`... - --> mutual_recursion_trait.rs:18:1 +error: Mutually recursive functions: when calling `::foo`... + --> mutual_recursion_trait.rs:12:5 | -18 | fn bar() { - | ^^^^^^^^ +12 | fn foo() { + | ^^^^^^^^ | -note: then `bar` calls `::foo`... - --> mutual_recursion_trait.rs:19:5 - | -19 | ::foo(); - | ^^^^^^^^^^^^^^^^^^^ -note: finally `::foo` calls `bar`. +note: then `::foo` calls `bar`... --> mutual_recursion_trait.rs:13:9 | 13 | bar(); | ^^^^^ +note: finally `bar` calls `::foo`. + --> mutual_recursion_trait.rs:19:5 + | +19 | ::foo(); + | ^^^^^^^^^^^^^^^^^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/terminates/recursion_through_contract.stderr b/creusot/tests/should_fail/terminates/recursion_through_contract.stderr index 7e5a38ec8c..3703aa321e 100644 --- a/creusot/tests/should_fail/terminates/recursion_through_contract.stderr +++ b/creusot/tests/should_fail/terminates/recursion_through_contract.stderr @@ -1,36 +1,36 @@ -error: Mutually recursive functions: when calling `f2`... - --> recursion_through_contract.rs:23:1 +error: Mutually recursive functions: when calling `with_requires`... + --> recursion_through_contract.rs:20:1 | -23 | fn f2() -> Int { - | ^^^^^^^^^^^^^^ +20 | fn with_requires(x: Int) {} + | ^^^^^^^^^^^^^^^^^^^^^^^^ | -note: then `f2` calls `with_requires`... - --> recursion_through_contract.rs:24:5 - | -24 | with_requires(5); - | ^^^^^^^^^^^^^^^^ -note: finally `with_requires` calls `f2`. +note: then `with_requires` calls `f2`... --> recursion_through_contract.rs:19:17 | 19 | #[requires(x == f2())] | ^^^^ - -error: Mutually recursive functions: when calling `f1`... - --> recursion_through_contract.rs:13:1 +note: finally `f2` calls `with_requires`. + --> recursion_through_contract.rs:24:5 | -13 | fn f1() -> Int { - | ^^^^^^^^^^^^^^ +24 | with_requires(5); + | ^^^^^^^^^^^^^^^^ + +error: Mutually recursive functions: when calling `with_proof_assert`... + --> recursion_through_contract.rs:6:1 | -note: then `f1` calls `with_proof_assert`... - --> recursion_through_contract.rs:14:5 +6 | fn with_proof_assert(x: Int) { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -14 | with_proof_assert(5); - | ^^^^^^^^^^^^^^^^^^^^ -note: finally `with_proof_assert` calls `f1`. +note: then `with_proof_assert` calls `f1`... --> recursion_through_contract.rs:8:14 | 8 | x == f1() | ^^^^ +note: finally `f1` calls `with_proof_assert`. + --> recursion_through_contract.rs:14:5 + | +14 | with_proof_assert(5); + | ^^^^^^^^^^^^^^^^^^^^ error: aborting due to 2 previous errors diff --git a/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml b/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml new file mode 100644 index 0000000000..848fefd858 --- /dev/null +++ b/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz b/creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..6c062414134dec9aca0f933e6f0706a6768e0b72 GIT binary patch literal 105 zcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!5cS@%0Hd_u$dgJ>l6J7_)LG ztLoH`314Gko~cb+sX6VLm>L^fXWKKilVY80Zkp4kO*?t) + + + + + + diff --git a/creusot/tests/should_succeed/termination/default_impl/why3shapes.gz b/creusot/tests/should_succeed/termination/default_impl/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..8039d107e60d7999ed0f63df0240e8d413a7ba34 GIT binary patch literal 45 xcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!3RgVo;m=MqCo83IJJ{58wa* literal 0 HcmV?d00001 diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml new file mode 100644 index 0000000000..420c651bbd --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml @@ -0,0 +1,8 @@ + + + + + + + diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..8039d107e60d7999ed0f63df0240e8d413a7ba34 GIT binary patch literal 45 xcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!3RgVo;m=MqCo83IJJ{58wa* literal 0 HcmV?d00001