diff --git a/docs/src/getting-started/verification-results/failure_example.expected b/docs/src/getting-started/verification-results/failure_example.expected index 7df34043cdf7..a5483fa08c71 100644 --- a/docs/src/getting-started/verification-results/failure_example.expected +++ b/docs/src/getting-started/verification-results/failure_example.expected @@ -1,2 +1,2 @@ FAILURE\ -Description: "assertion failed: arr.len() != 3" +Description: "Panic: assertion failed: arr.len() != 3" diff --git a/docs/src/getting-started/verification-results/success_example.expected b/docs/src/getting-started/verification-results/success_example.expected index 65cb0eb8b288..b3f03fb9ef64 100644 --- a/docs/src/getting-started/verification-results/success_example.expected +++ b/docs/src/getting-started/verification-results/success_example.expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "assertion failed: sum == 6" +Description: "Panic: assertion failed: sum == 6" diff --git a/docs/src/getting-started/verification-results/undetermined_example.expected b/docs/src/getting-started/verification-results/undetermined_example.expected index 273ef21610de..3511f35ce57d 100644 --- a/docs/src/getting-started/verification-results/undetermined_example.expected +++ b/docs/src/getting-started/verification-results/undetermined_example.expected @@ -1,2 +1,2 @@ UNDETERMINED\ -Description: "assertion failed: x == 0" +Description: "Panic: assertion failed: x == 0" diff --git a/docs/src/getting-started/verification-results/unreachable_example.expected b/docs/src/getting-started/verification-results/unreachable_example.expected index 9beb5ee416fa..b464e91710d0 100644 --- a/docs/src/getting-started/verification-results/unreachable_example.expected +++ b/docs/src/getting-started/verification-results/unreachable_example.expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: x < 8" +Description: "Panic: assertion failed: x < 8" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 2392a801809f..5781850557b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -231,7 +231,7 @@ impl GotocCtx<'_> { // If there is one in the MIR, use it; otherwise, explain that we can't. assert!(!fargs.is_empty(), "Panic requires a string message"); let msg = self.extract_const_message(&fargs[0]).unwrap_or(String::from( - "This is a placeholder message; Kani doesn't support message formatted at runtime", + "Panic: This is a placeholder message; Kani doesn't support message formatted at runtime", )); self.codegen_fatal_error(PropertyClass::Assertion, &msg, span) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index eabc861b8fb7..5e06a2889567 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -261,7 +261,7 @@ impl GotocCtx<'_> { // "index out of bounds: the length is {len} but the index is {index}", // but CBMC only accepts static messages so we don't add values to the message. ( - "index out of bounds: the length is less than or equal to the given index", + "Panic: index out of bounds: the length is less than or equal to the given index".to_string(), PropertyClass::Assertion, ) } @@ -270,22 +270,23 @@ impl GotocCtx<'_> { // Generate a generic one here. ( "misaligned pointer dereference: address must be a multiple of its type's \ - alignment", + alignment".to_string(), PropertyClass::SafetyCheck, ) } // For all other assert kind we can get the static message. AssertMessage::NullPointerDereference => { - (msg.description().unwrap(), PropertyClass::SafetyCheck) + (msg.description().unwrap().to_string(), PropertyClass::SafetyCheck) } AssertMessage::Overflow { .. } | AssertMessage::OverflowNeg { .. } | AssertMessage::DivisionByZero { .. } | AssertMessage::RemainderByZero { .. } | AssertMessage::ResumedAfterReturn { .. } - | AssertMessage::ResumedAfterPanic { .. } => { - (msg.description().unwrap(), PropertyClass::Assertion) - } + | AssertMessage::ResumedAfterPanic { .. } => ( + "Panic: ".to_owned() + msg.description().unwrap(), + PropertyClass::Assertion, + ), }; let (msg_str, reach_stmt) = diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index e54a1fc4dd9e..9a8764a4701e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -137,7 +137,12 @@ impl GotocHook for Assert { Stmt::block( vec![ reach_stmt, - gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc), + gcx.codegen_assert_assume( + cond, + PropertyClass::Assertion, + &("Panic: ".to_owned() + &msg), + caller_loc, + ), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -272,7 +277,12 @@ impl GotocHook for Check { Stmt::block( vec![ reach_stmt, - gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), + gcx.codegen_assert( + cond, + PropertyClass::Assertion, + &("Panic: ".to_owned() + &msg), + caller_loc, + ), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, diff --git a/tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected b/tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected index 9d9eafbffb57..1112410a2e40 100644 --- a/tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected +++ b/tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected @@ -1,2 +1,2 @@ Status: SUCCESS\ -Description: "assertion failed: x * y == 33" +Description: "Panic: assertion failed: x * y == 33" diff --git a/tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected b/tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected index 439f93c26286..0d9ba19a8961 100644 --- a/tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected +++ b/tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected @@ -1,2 +1,2 @@ Status: SUCCESS\ -Description: "assertion failed: x == 98" +Description: "Panic: assertion failed: x == 98" diff --git a/tests/cargo-kani/assert-reach/test.expected b/tests/cargo-kani/assert-reach/test.expected index c98b7af7d812..d93f9b1182e7 100644 --- a/tests/cargo-kani/assert-reach/test.expected +++ b/tests/cargo-kani/assert-reach/test.expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: z == x - 1" +Description: "Panic: assertion failed: z == x - 1" diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected index 97d4b6c54c09..ad793d083e70 100644 --- a/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected +++ b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected @@ -1,4 +1,4 @@ Status: SUCCESS\ -Description: "assertion failed: C.x == 0" +Description: "Panic: assertion failed: C.x == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected index 97d4b6c54c09..ad793d083e70 100644 --- a/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected +++ b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected @@ -1,4 +1,4 @@ Status: SUCCESS\ -Description: "assertion failed: C.x == 0" +Description: "Panic: assertion failed: C.x == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/demos/non-empty-range/check_range.expected b/tests/cargo-kani/demos/non-empty-range/check_range.expected index c0c666fca101..7ec055972e3a 100644 --- a/tests/cargo-kani/demos/non-empty-range/check_range.expected +++ b/tests/cargo-kani/demos/non-empty-range/check_range.expected @@ -1,4 +1,4 @@ Status: SUCCESS\ -Description: "assertion failed: range.is_none() || !range.as_ref().unwrap().is_empty()" +Description: "Panic: assertion failed: range.is_none() || !range.as_ref().unwrap().is_empty()" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/itoa_dep/check_unsigned.expected b/tests/cargo-kani/itoa_dep/check_unsigned.expected index 5281b6338980..e4641850e2ca 100644 --- a/tests/cargo-kani/itoa_dep/check_unsigned.expected +++ b/tests/cargo-kani/itoa_dep/check_unsigned.expected @@ -1,4 +1,4 @@ Status: SUCCESS\ -Description: "assertion failed: result == &output" +Description: "Panic: assertion failed: result == &output" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/nested-dirs/crate1/a_check.expected b/tests/cargo-kani/nested-dirs/crate1/a_check.expected index b380023f5c4d..a363a0736743 100644 --- a/tests/cargo-kani/nested-dirs/crate1/a_check.expected +++ b/tests/cargo-kani/nested-dirs/crate1/a_check.expected @@ -1,3 +1,3 @@ Status: SUCCESS\ -Description: "assertion failed: v.len() == 3" +Description: "Panic: assertion failed: v.len() == 3" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/nested-dirs/crate2/another_check.expected b/tests/cargo-kani/nested-dirs/crate2/another_check.expected index f2ff925eb096..c14421848cd1 100644 --- a/tests/cargo-kani/nested-dirs/crate2/another_check.expected +++ b/tests/cargo-kani/nested-dirs/crate2/another_check.expected @@ -1,3 +1,3 @@ Status: SUCCESS\ -Description: "assertion failed: result == 4" +Description: "Panic: assertion failed: result == 4" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/nested-dirs/crate2/nested_crate/yet_another_check.expected b/tests/cargo-kani/nested-dirs/crate2/nested_crate/yet_another_check.expected index 4e8e037b84a8..81f05fcff1a7 100644 --- a/tests/cargo-kani/nested-dirs/crate2/nested_crate/yet_another_check.expected +++ b/tests/cargo-kani/nested-dirs/crate2/nested_crate/yet_another_check.expected @@ -1,4 +1,4 @@ Status: SUCCESS\ -Description: "assertion failed: y - x == 0" +Description: "Panic: assertion failed: y - x == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/output-format/main.expected b/tests/cargo-kani/output-format/main.expected index 71f79815bdc1..cdf545098271 100644 --- a/tests/cargo-kani/output-format/main.expected +++ b/tests/cargo-kani/output-format/main.expected @@ -1 +1 @@ -Description: "assertion failed: 1 + 1 == 2" +Description: "Panic: assertion failed: 1 + 1 == 2" diff --git a/tests/cargo-kani/small-vec/check_vec.expected b/tests/cargo-kani/small-vec/check_vec.expected index a7c1d04f3f19..ca0238e0ed60 100644 --- a/tests/cargo-kani/small-vec/check_vec.expected +++ b/tests/cargo-kani/small-vec/check_vec.expected @@ -1,5 +1,5 @@ Status: SUCCESS\ -Description: "assertion failed: c < char::MAX"\ +Description: "Panic: assertion failed: c < char::MAX"\ in function check_vec VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/stubbing-ws-packages/expected b/tests/cargo-kani/stubbing-ws-packages/expected index 181be1e37ccd..fe1d0a64d7a2 100644 --- a/tests/cargo-kani/stubbing-ws-packages/expected +++ b/tests/cargo-kani/stubbing-ws-packages/expected @@ -1,25 +1,25 @@ Checking harness verify::check_no_stub... Status: SUCCESS\ -Description: "assertion failed: config == StubConfig::NoStub" +Description: "Panic: assertion failed: config == StubConfig::NoStub" VERIFICATION:- SUCCESSFUL Checking harness verify::check_stub_1... Status: SUCCESS\ -Description: "assertion failed: config == StubConfig::Stub1" +Description: "Panic: assertion failed: config == StubConfig::Stub1" VERIFICATION:- SUCCESSFUL Checking harness verify_top::check_no_stub... Status: SUCCESS\ -Description: "assertion failed: stub_id() == None" +Description: "Panic: assertion failed: stub_id() == None" VERIFICATION:- SUCCESSFUL Checking harness verify_top::check_stub_1... Status: SUCCESS\ -Description: "assertion failed: stub_id() == Some(1)" +Description: "Panic: assertion failed: stub_id() == Some(1)" VERIFICATION:- SUCCESSFUL Checking harness verify_top::check_stub_2... Status: SUCCESS\ -Description: "assertion failed: stub_id() == Some(2)" +Description: "Panic: assertion failed: stub_id() == Some(2)" Complete - 5 successfully verified harnesses, 0 failures, 5 total. diff --git a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected index 1b18a4656c4f..5d804dbb87d3 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected @@ -1,17 +1,17 @@ fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ -Description: "assertion failed: self.head < self.tail" +Description: "Panic: assertion failed: self.head < self.tail" fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ -Description: "assertion failed: self.head < self.cap()" +Description: "Panic: assertion failed: self.head < self.cap()" fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ -Description: "assertion failed: self.tail < self.cap()" +Description: "Panic: assertion failed: self.tail < self.cap()" fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ -Description: "assertion failed: self.cap().count_ones() == 1" +Description: "Panic: assertion failed: self.cap().count_ones() == 1" VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected index 2fa924c89f3f..71740f901d46 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected @@ -1,6 +1,6 @@ cve::VecDeque::::handle_capacity_increase.assertion\ - Status: FAILURE\ -- Description: "assertion failed: self.head < self.cap()" +- Description: "Panic: assertion failed: self.head < self.cap()" Location: src/cve.rs -Failed Checks: assertion failed: self.head < self.cap() +Failed Checks: Panic: assertion failed: self.head < self.cap() diff --git a/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected b/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected index 2d1e4f06ed8a..121595103596 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected @@ -1,16 +1,16 @@ cve::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.head < self.cap()"\ +Description: "Panic: assertion failed: self.head < self.cap()"\ Location: src/cve.rs cve::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.tail < self.cap()"\ +Description: "Panic: assertion failed: self.tail < self.cap()"\ Location: src/cve.rs cve::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.cap().count_ones() == 1"\ +Description: "Panic: assertion failed: self.cap().count_ones() == 1"\ Location: src/cve.rs VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected b/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected index 7dc9db7ef9b7..154aa39e3c35 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected @@ -1,16 +1,16 @@ fixed::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.head < self.cap()"\ +Description: "Panic: assertion failed: self.head < self.cap()"\ Location: src/fixed.rs fixed::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.tail < self.cap()"\ +Description: "Panic: assertion failed: self.tail < self.cap()"\ Location: src/fixed.rs fixed::VecDeque::::handle_capacity_increase.assertion\ Status: SUCCESS\ -Description: "assertion failed: self.cap().count_ones() == 1"\ +Description: "Panic: assertion failed: self.cap().count_ones() == 1"\ Location: src/fixed.rs VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/abort/expected b/tests/expected/abort/expected index aaa02359094c..169f9e48cbee 100644 --- a/tests/expected/abort/expected +++ b/tests/expected/abort/expected @@ -1,5 +1,5 @@ Status: UNREACHABLE\ -Description: ""This is unreachable""\ +Description: "Panic: "This is unreachable""\ in function main Status: FAILURE\ diff --git a/tests/expected/arbitrary/duration.expected b/tests/expected/arbitrary/duration.expected index bef13c5e7739..3a0319519209 100644 --- a/tests/expected/arbitrary/duration.expected +++ b/tests/expected/arbitrary/duration.expected @@ -19,7 +19,7 @@ Status: SATISFIED\ Description: "Max nanos" Status: SUCCESS\ -Description: ""Is Zero"" +Description: "Panic: "Is Zero"" 6 of 6 cover properties satisfied 1 successfully verified harnesses, 0 failures diff --git a/tests/expected/arbitrary/ptrs/pointer_generator.expected b/tests/expected/arbitrary/ptrs/pointer_generator.expected index 4627d354aebb..21e26481333b 100644 --- a/tests/expected/arbitrary/ptrs/pointer_generator.expected +++ b/tests/expected/arbitrary/ptrs/pointer_generator.expected @@ -1,21 +1,21 @@ Checking harness check_arbitrary_ptr... Status: SUCCESS\ -Description: ""OutOfBounds"" +Description: "Panic: "OutOfBounds"" Status: SUCCESS\ -Description: ""InBounds"" +Description: "Panic: "InBounds"" Status: SUCCESS\ -Description: ""NullPtr"" +Description: "Panic: "NullPtr"" Status: FAILURE\ -Description: ""DeadObject"" +Description: "Panic: "DeadObject"" Status: SATISFIED\ Description: "Dangling" Status: UNREACHABLE\ -Description: ""Dangling write"" +Description: "Panic: "Dangling write"" Verification failed for - check_arbitrary_ptr diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.expected b/tests/expected/arbitrary/ptrs/pointer_inbounds.expected index 838829163a36..0849bbd9d691 100644 --- a/tests/expected/arbitrary/ptrs/pointer_inbounds.expected +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.expected @@ -15,15 +15,15 @@ Description: "Smaller" Checking harness check_alignment... Status: SUCCESS\ -Description: ""Aligned"" +Description: "Panic: "Aligned"" Status: SUCCESS\ -Description: ""Unaligned"" +Description: "Panic: "Unaligned"" Checking harness check_inbounds_initialized... Status: SUCCESS\ -Description: ""ValidRead"" +Description: "Panic: "ValidRead"" Checking harness check_inbounds... @@ -34,6 +34,6 @@ Status: SATISFIED\ Description: "Initialized" Status: SUCCESS\ -Description: ""ValidWrite"" +Description: "Panic: "ValidWrite"" Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/expected/arith_checks/expected b/tests/expected/arith_checks/expected index eec22e8235c7..9d05a8650b6e 100644 --- a/tests/expected/arith_checks/expected +++ b/tests/expected/arith_checks/expected @@ -1 +1 @@ -Failed Checks: attempt to subtract with overflow +Failed Checks: Panic: attempt to subtract with overflow diff --git a/tests/expected/assert-eq-chained/expected b/tests/expected/assert-eq-chained/expected index 9f02ab7caa3c..1b8e218b3349 100644 --- a/tests/expected/assert-eq-chained/expected +++ b/tests/expected/assert-eq-chained/expected @@ -1,13 +1,13 @@ Status: SUCCESS\ -Description: "assertion failed: x > 3 == true" +Description: "Panic: assertion failed: x > 3 == true" Status: SUCCESS\ -Description: "assertion failed: x == 1 == false" +Description: "Panic: assertion failed: x == 1 == false" Status: SUCCESS\ -Description: "assertion failed: x < 10 != false" +Description: "Panic: assertion failed: x < 10 != false" Status: FAILURE\ -Description: "assertion failed: x == 7 != false" +Description: "Panic: assertion failed: x == 7 != false" VERIFICATION:- FAILED diff --git a/tests/expected/assert-location/assert-false/expected b/tests/expected/assert-location/assert-false/expected index 54cbbe9ab07b..e9db654fd4df 100644 --- a/tests/expected/assert-location/assert-false/expected +++ b/tests/expected/assert-location/assert-false/expected @@ -1,3 +1,3 @@ -line 18 assertion failed: false: FAILURE -line 23 "{}", s: FAILURE -line 27 "Fail with custom static message": FAILURE +line 18 Panic: assertion failed: false: FAILURE +line 23 Panic: "{}", s: FAILURE +line 27 Panic: "Fail with custom static message": FAILURE diff --git a/tests/expected/assert-location/debug-assert/expected b/tests/expected/assert-location/debug-assert/expected index d32257a7c90d..c49775461a66 100644 --- a/tests/expected/assert-location/debug-assert/expected +++ b/tests/expected/assert-location/debug-assert/expected @@ -1,2 +1,2 @@ -line 13 "This should fail and stop the execution": FAILURE -line 14 "This should be unreachable": SUCCESS +line 13 Panic: "This should fail and stop the execution": FAILURE +line 14 Panic: "This should be unreachable": SUCCESS diff --git a/tests/expected/coroutines/expected b/tests/expected/coroutines/expected index c1be99367ed3..2b8ac2c98837 100644 --- a/tests/expected/coroutines/expected +++ b/tests/expected/coroutines/expected @@ -1,10 +1,10 @@ SUCCESS\ -Description: "assertion failed: res == CoroutineState::Yielded(val)" +Description: "Panic: assertion failed: res == CoroutineState::Yielded(val)" SUCCESS\ -Description: "assertion failed: res == CoroutineState::Complete(!val)" +Description: "Panic: assertion failed: res == CoroutineState::Complete(!val)" UNREACHABLE\ -Description: "coroutine resumed after completion" +Description: "Panic: coroutine resumed after completion" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/coroutines/pin/expected b/tests/expected/coroutines/pin/expected index 1c2dc54a2f62..d1bbdb1986aa 100644 --- a/tests/expected/coroutines/pin/expected +++ b/tests/expected/coroutines/pin/expected @@ -7,7 +7,7 @@ Description: "unexpected yield from resume"\ in function main UNREACHABLE\ -Description: "coroutine resumed after completion" +Description: "Panic: coroutine resumed after completion" in function main::{closure#0} VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected index f35f18084911..f542c56ca721 100644 --- a/tests/expected/derive-arbitrary/safety_constraint_helper/expected +++ b/tests/expected/derive-arbitrary/safety_constraint_helper/expected @@ -1,17 +1,17 @@ Check 1: check_invariant_helper_ok.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.x >= 0" + - Description: "Panic: assertion failed: pos_point.x >= 0" Check 2: check_invariant_helper_ok.assertion.2\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.y >= 0" + - Description: "Panic: assertion failed: pos_point.y >= 0" Check 1: check_invariant_helper_fail.assertion.1\ - Status: FAILURE\ - - Description: "assertion failed: pos_point.x >= 0" + - Description: "Panic: assertion failed: pos_point.x >= 0" Check 2: check_invariant_helper_fail.assertion.2\ - Status: FAILURE\ - - Description: "assertion failed: pos_point.y >= 0" + - Description: "Panic: assertion failed: pos_point.y >= 0" Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/expected b/tests/expected/derive-invariant/attrs_cfg_guard/expected index edb3e256975d..81541c3feed1 100644 --- a/tests/expected/derive-invariant/attrs_cfg_guard/expected +++ b/tests/expected/derive-invariant/attrs_cfg_guard/expected @@ -1,9 +1,9 @@ Check 1: check_safety_constraint_cfg.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.x >= 0" + - Description: "Panic: assertion failed: pos_point.x >= 0" Check 2: check_safety_constraint_cfg.assertion.2\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.y >= 0" + - Description: "Panic: assertion failed: pos_point.y >= 0" Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/attrs_mixed/expected b/tests/expected/derive-invariant/attrs_mixed/expected index edb3e256975d..81541c3feed1 100644 --- a/tests/expected/derive-invariant/attrs_mixed/expected +++ b/tests/expected/derive-invariant/attrs_mixed/expected @@ -1,9 +1,9 @@ Check 1: check_safety_constraint_cfg.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.x >= 0" + - Description: "Panic: assertion failed: pos_point.x >= 0" Check 2: check_safety_constraint_cfg.assertion.2\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.y >= 0" + - Description: "Panic: assertion failed: pos_point.y >= 0" Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/empty_struct/expected b/tests/expected/derive-invariant/empty_struct/expected index 8fdca72b1ead..ff72c86f381f 100644 --- a/tests/expected/derive-invariant/empty_struct/expected +++ b/tests/expected/derive-invariant/empty_struct/expected @@ -1,8 +1,8 @@ - Status: SUCCESS\ - - Description: "assertion failed: void1.is_safe()" + - Description: "Panic: assertion failed: void1.is_safe()" - Status: SUCCESS\ - - Description: "assertion failed: void2.is_safe()" + - Description: "Panic: assertion failed: void2.is_safe()" - Status: SUCCESS\ - - Description: "assertion failed: void3.is_safe()" + - Description: "Panic: assertion failed: void3.is_safe()" diff --git a/tests/expected/derive-invariant/generic_struct/expected b/tests/expected/derive-invariant/generic_struct/expected index 5e5886bb3e45..591c0dba6d0c 100644 --- a/tests/expected/derive-invariant/generic_struct/expected +++ b/tests/expected/derive-invariant/generic_struct/expected @@ -1,2 +1,2 @@ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "Panic: assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/named_struct/expected b/tests/expected/derive-invariant/named_struct/expected index 5e5886bb3e45..591c0dba6d0c 100644 --- a/tests/expected/derive-invariant/named_struct/expected +++ b/tests/expected/derive-invariant/named_struct/expected @@ -1,2 +1,2 @@ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "Panic: assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/safety_constraint_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected index 31b6de54c647..2fc2156a8eea 100644 --- a/tests/expected/derive-invariant/safety_constraint_helper/expected +++ b/tests/expected/derive-invariant/safety_constraint_helper/expected @@ -1,13 +1,13 @@ Check 1: check_invariant_helper_ok.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Check 1: check_invariant_helper_ok_manual.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Check 1: check_invariant_helper_fail.assertion.1\ - Status: FAILURE\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected index 31b6de54c647..2fc2156a8eea 100644 --- a/tests/expected/derive-invariant/safety_constraint_helper_funs/expected +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected @@ -1,13 +1,13 @@ Check 1: check_invariant_helper_ok.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Check 1: check_invariant_helper_ok_manual.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Check 1: check_invariant_helper_fail.assertion.1\ - Status: FAILURE\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/safety_invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected index 511d5901e154..bacb5eeb89f9 100644 --- a/tests/expected/derive-invariant/safety_invariant_fail/expected +++ b/tests/expected/derive-invariant/safety_invariant_fail/expected @@ -1,4 +1,4 @@ - Status: FAILURE\ - - Description: "assertion failed: wrapper.is_safe()" + - Description: "Panic: assertion failed: wrapper.is_safe()" Verification failed for - check_invariant_fail diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected index 0853a68fa79e..c42021e3918e 100644 --- a/tests/expected/derive-invariant/safety_invariant_fail_mut/expected +++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected @@ -1,10 +1,10 @@ Check 1: check_invariant_fail_mut.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" Check 2: check_invariant_fail_mut.assertion.2\ - Status: FAILURE\ - - Description: "assertion failed: pos_point.is_safe()" + - Description: "Panic: assertion failed: pos_point.is_safe()" VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) diff --git a/tests/expected/derive-invariant/unnamed_struct/expected b/tests/expected/derive-invariant/unnamed_struct/expected index 5e5886bb3e45..591c0dba6d0c 100644 --- a/tests/expected/derive-invariant/unnamed_struct/expected +++ b/tests/expected/derive-invariant/unnamed_struct/expected @@ -1,2 +1,2 @@ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "Panic: assertion failed: point.is_safe()" diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 4b70f8364e05..5ab773ebfffc 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,6 +1,6 @@ assertion\ - Status: FAILURE\ -- Description: "|result : &u32| *result == x"\ +- Description: "Panic: |result : &u32| *result == x"\ in function max VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index 9eee213789b9..c83b8da541dd 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|result : &u32| *result == x || *result == y"\ +- Description: "Panic: |result : &u32| *result == x || *result == y"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index 179430b8a249..a38c8b4365dc 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -1,4 +1,4 @@ assertion\ - Status: FAILURE\ -- Description: "attempt to divide by zero"\ +- Description: "Panic: attempt to divide by zero"\ arbitrary_requires_fail.rs:7:5 diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.expected b/tests/expected/function-contract/as-assertions/assert-postconditions.expected index e16069ec2fad..14ce899f6f1e 100644 --- a/tests/expected/function-contract/as-assertions/assert-postconditions.expected +++ b/tests/expected/function-contract/as-assertions/assert-postconditions.expected @@ -1,9 +1,9 @@ assertion\ - Status: FAILURE\ - - Description: "|_| old(*add_two_ptr + 1) == *add_two_ptr" + - Description: "Panic: |_| old(*add_two_ptr + 1) == *add_two_ptr" assertion\ - Status: SUCCESS\ - - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr" + - Description: "Panic: |_| old(*add_one_ptr + 1) == *add_one_ptr" VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.expected b/tests/expected/function-contract/as-assertions/assert-preconditions.expected index ac31f337cc33..42f2655aea96 100644 --- a/tests/expected/function-contract/as-assertions/assert-preconditions.expected +++ b/tests/expected/function-contract/as-assertions/assert-preconditions.expected @@ -1,14 +1,14 @@ assertion\ - Status: FAILURE\ - - Description: "*ptr < 100" + - Description: "Panic: *ptr < 100" assertion\ - Status: FAILURE\ - - Description: "*ptr == 4" + - Description: "Panic: *ptr == 4" assertion\ - Status: FAILURE\ - - Description: "*ptr < 100" + - Description: "Panic: *ptr < 100" Summary: Verification failed for - prove_add_one diff --git a/tests/expected/function-contract/as-assertions/loops.expected b/tests/expected/function-contract/as-assertions/loops.expected index 711b7e311014..6bef68408ad8 100644 --- a/tests/expected/function-contract/as-assertions/loops.expected +++ b/tests/expected/function-contract/as-assertions/loops.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ - - Description: "x != 0 && y != 0" + - Description: "Panic: x != 0 && y != 0" assertion\ - Status: SUCCESS\ - - Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0" + - Description: "Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/as-assertions/precedence.expected b/tests/expected/function-contract/as-assertions/precedence.expected index 0fa0efc5b0fc..70594dfdc215 100644 --- a/tests/expected/function-contract/as-assertions/precedence.expected +++ b/tests/expected/function-contract/as-assertions/precedence.expected @@ -1,34 +1,34 @@ assertion\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" assertion\ - Status: SUCCESS\ - - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr" + - Description: "Panic: |_| old(*add_one_ptr + 1) == *add_one_ptr" assertion\ - Status: UNREACHABLE\ - - Description: "*add_one_ptr == 4" + - Description: "Panic: *add_one_ptr == 4" assertion\ - Status: UNREACHABLE\ - - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr" + - Description: "Panic: |_| old(*add_one_ptr + 1) == *add_one_ptr" assertion\ - Status: SUCCESS\ - - Description: "*add_three_ptr < 100" + - Description: "Panic: *add_three_ptr < 100" assertion\ - Status: SUCCESS\ - - Description: "*add_two_ptr < 101" + - Description: "Panic: *add_two_ptr < 101" assertion\ - Status: SUCCESS\ - - Description: "|_| old(*add_two_ptr + 2) == *add_two_ptr" + - Description: "Panic: |_| old(*add_two_ptr + 2) == *add_two_ptr" assertion\ - Status: SUCCESS\ - - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr" + - Description: "Panic: |_| old(*add_one_ptr + 1) == *add_one_ptr" Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected index e181e6b2ad17..53fc2f156686 100644 --- a/tests/expected/function-contract/checking_from_external_mod.expected +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ -- Description: "|result : &u32| (*result == x) | (*result == y)"\ +- Description: "Panic: |result : &u32| (*result == x) | (*result == y)"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected index cfe84c06fc85..f5759ea5d41b 100644 --- a/tests/expected/function-contract/checking_in_impl.expected +++ b/tests/expected/function-contract/checking_in_impl.expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ -- Description: "|result : &WrappedInt| (*result == self) | (*result == y)"\ +- Description: "Panic: |result : &WrappedInt| (*result == self) | (*result == y)"\ in function WrappedInt::max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected index 79cc3d572af0..5cad2f4faab9 100644 --- a/tests/expected/function-contract/fail_on_two.expected +++ b/tests/expected/function-contract/fail_on_two.expected @@ -7,6 +7,6 @@ Failed Checks: internal error: entered unreachable code: fail on two assertion\ - Status: FAILURE\ -- Description: "|result : &i32| *result < 3" +- Description: "Panic: |result : &i32| *result < 3" -Failed Checks: |result : &i32| *result < 3 +Failed Checks: Panic: |result : &i32| *result < 3 diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index ca21817c8329..945a83933163 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ +- Description: "Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ in function gcd -Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 +Failed Checks: Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected index 4bb02ab36f49..09d813c0c13d 100644 --- a/tests/expected/function-contract/gcd_failure_contract.expected +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "|result : &T| *result != 0 && x % *result == 1 && y % *result == 0"\ +- Description: "Panic: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0"\ in function gcd\ -Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 +Failed Checks: Panic: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected index 863392098be4..7b935f05725b 100644 --- a/tests/expected/function-contract/gcd_rec_code_fail.expected +++ b/tests/expected/function-contract/gcd_rec_code_fail.expected @@ -1,3 +1,3 @@ -Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 +Failed Checks: Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected index 0556bfc50204..009e5eb62c94 100644 --- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ -- Description: "x != 0 && y != 0" +- Description: "Panic: x != 0 && y != 0" assertion\ - Status: SUCCESS\ -- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0" +- Description: "Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected index 6cc0354ca89a..52fc8ce20e6c 100644 --- a/tests/expected/function-contract/gcd_rec_contract_fail.expected +++ b/tests/expected/function-contract/gcd_rec_contract_fail.expected @@ -1,3 +1,3 @@ -Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 +Failed Checks: Panic: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected index b522716cc001..de7ee8a35430 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -1,17 +1,17 @@ Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: self.num % f2.num == 0" +- Description: "Panic: assertion failed: self.num % f2.num == 0" Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: self.den % f2.den == 0" +- Description: "Panic: assertion failed: self.den % f2.den == 0" Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: gcd1 == gcd2" +- Description: "Panic: assertion failed: gcd1 == gcd2" .assertion\ - Status: SUCCESS\ -- Description: "x != 0 && y != 0" +- Description: "Panic: x != 0 && y != 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected index 0556bfc50204..009e5eb62c94 100644 --- a/tests/expected/function-contract/gcd_rec_simple_pass.expected +++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ -- Description: "x != 0 && y != 0" +- Description: "Panic: x != 0 && y != 0" assertion\ - Status: SUCCESS\ -- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0" +- Description: "Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_replacement_fail.expected b/tests/expected/function-contract/gcd_replacement_fail.expected index a993325bd5e5..4d5d83bb89dd 100644 --- a/tests/expected/function-contract/gcd_replacement_fail.expected +++ b/tests/expected/function-contract/gcd_replacement_fail.expected @@ -1,17 +1,17 @@ Frac::check_equals.assertion\ - Status: FAILURE\ -- Description: "attempt to calculate the remainder with a divisor of zero" +- Description: "Panic: attempt to calculate the remainder with a divisor of zero" Frac::check_equals.assertion\ - Status: FAILURE\ -- Description: "assertion failed: self.den % f2.den == 0" +- Description: "Panic: assertion failed: self.den % f2.den == 0" Frac::check_equals.assertion\ - Status: FAILURE\ -- Description: "assertion failed: gcd1 == gcd2" +- Description: "Panic: assertion failed: gcd1 == gcd2" -Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: assertion failed: self.den % f2.den == 0 -Failed Checks: assertion failed: gcd1 == gcd2 +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero +Failed Checks: Panic: assertion failed: self.den % f2.den == 0 +Failed Checks: Panic: assertion failed: gcd1 == gcd2 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected index 1c6df8455267..5191b6968884 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -1,17 +1,17 @@ .assertion\ - Status: SUCCESS\ -- Description: "x != 0 && y != 0" +- Description: "Panic: x != 0 && y != 0" Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: self.num % f2.num == 0" +- Description: "Panic: assertion failed: self.num % f2.num == 0" Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: self.den % f2.den == 0" +- Description: "Panic: assertion failed: self.den % f2.den == 0" Frac::check_equals.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: gcd1 == gcd2" +- Description: "Panic: assertion failed: gcd1 == gcd2" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected index e5885dd11179..3c47f5c9fe02 100644 --- a/tests/expected/function-contract/gcd_success.expected +++ b/tests/expected/function-contract/gcd_success.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ +- Description: "Panic: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ in function gcd VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/block.expected b/tests/expected/function-contract/history/block.expected index 83e958f52d77..f37aa97dced6 100644 --- a/tests/expected/function-contract/history/block.expected +++ b/tests/expected/function-contract/history/block.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ - - Description: "|result| old({ let x = &ptr; let y = **x; y + 1 }) == *ptr"\ + - Description: "Panic: |result| old({ let x = &ptr; let y = **x; y + 1 }) == *ptr"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/clone_pass.expected b/tests/expected/function-contract/history/clone_pass.expected index bebbe1ae8834..22d04cd4a6dd 100644 --- a/tests/expected/function-contract/history/clone_pass.expected +++ b/tests/expected/function-contract/history/clone_pass.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ - - Description: "|result| old(ptr.clone()).0 + 1 == ptr.0"\ + - Description: "Panic: |result| old(ptr.clone()).0 + 1 == ptr.0"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/copy_pass.expected b/tests/expected/function-contract/history/copy_pass.expected index 40f15ebf64fa..acc3c66b6d3e 100644 --- a/tests/expected/function-contract/history/copy_pass.expected +++ b/tests/expected/function-contract/history/copy_pass.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ - - Description: "|result| old(ptr.0) + 1 == ptr.0"\ + - Description: "Panic: |result| old(ptr.0) + 1 == ptr.0"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/function_call.expected b/tests/expected/function-contract/history/function_call.expected index cba9ece7ed26..d7853944ca08 100644 --- a/tests/expected/function-contract/history/function_call.expected +++ b/tests/expected/function-contract/history/function_call.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ - - Description: "|result| old(add1(dereference(ptr))) == *ptr"\ + - Description: "Panic: |result| old(add1(dereference(ptr))) == *ptr"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/no_modifies.expected b/tests/expected/function-contract/history/no_modifies.expected index eb0178186987..9724251d8b0c 100644 --- a/tests/expected/function-contract/history/no_modifies.expected +++ b/tests/expected/function-contract/history/no_modifies.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ - - Description: "|result : &u32| old(val) == val && old(val.wrapping_add(1)) == *result"\ + - Description: "Panic: |result : &u32| old(val) == val && old(val.wrapping_add(1)) == *result"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected index a9e6a1a6a601..7bbe7d5021c1 100644 --- a/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected +++ b/tests/expected/function-contract/history/respects-preconditions/ensures_before_requires.expected @@ -1,5 +1,5 @@ next\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/respects-preconditions/modifies.expected b/tests/expected/function-contract/history/respects-preconditions/modifies.expected index 40dd76d9ce4d..f0fe57d8e45d 100644 --- a/tests/expected/function-contract/history/respects-preconditions/modifies.expected +++ b/tests/expected/function-contract/history/respects-preconditions/modifies.expected @@ -1,5 +1,5 @@ modify\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected index a9e6a1a6a601..7bbe7d5021c1 100644 --- a/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected +++ b/tests/expected/function-contract/history/respects-preconditions/requires_before_ensures.expected @@ -1,5 +1,5 @@ next\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/side_effect.expected b/tests/expected/function-contract/history/side_effect.expected index 386399c67941..423625e0033b 100644 --- a/tests/expected/function-contract/history/side_effect.expected +++ b/tests/expected/function-contract/history/side_effect.expected @@ -1,2 +1,2 @@ -Failed Checks: |result| old({ *ptr+=1; *ptr }) == _val +Failed Checks: Panic: |result| old({ *ptr+=1; *ptr }) == _val VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/history/simple_fail.expected b/tests/expected/function-contract/history/simple_fail.expected index 29e2af7cf7fa..f17700aa1f63 100644 --- a/tests/expected/function-contract/history/simple_fail.expected +++ b/tests/expected/function-contract/history/simple_fail.expected @@ -1,7 +1,7 @@ assertion\ - Status: FAILURE\ -- Description: "|_| old(*ptr) == *ptr" +- Description: "Panic: |_| old(*ptr) == *ptr" -Failed Checks: |_| old(*ptr) == *ptr +Failed Checks: Panic: |_| old(*ptr) == *ptr VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/history/simple_pass.expected b/tests/expected/function-contract/history/simple_pass.expected index 8c3d786e1909..6cb4cf1f5e68 100644 --- a/tests/expected/function-contract/history/simple_pass.expected +++ b/tests/expected/function-contract/history/simple_pass.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|result| old(*ptr + 1) == *ptr"\ +- Description: "Panic: |result| old(*ptr + 1) == *ptr"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/simple_pass_twice.expected b/tests/expected/function-contract/history/simple_pass_twice.expected index 7d0cb9bfa18d..c30d507d27d7 100644 --- a/tests/expected/function-contract/history/simple_pass_twice.expected +++ b/tests/expected/function-contract/history/simple_pass_twice.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ -- Description: "|result| old(*ptr + 1) == *ptr"\ +- Description: "Panic: |result| old(*ptr + 1) == *ptr"\ assertion\ - Status: SUCCESS\ -- Description: "|result| old(*ptr + 1) == *ptr"\ +- Description: "Panic: |result| old(*ptr + 1) == *ptr"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/history/stub.expected b/tests/expected/function-contract/history/stub.expected index 1d354c1cdf6c..591073702fbc 100644 --- a/tests/expected/function-contract/history/stub.expected +++ b/tests/expected/function-contract/history/stub.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ -- Description: "|result| old(*ptr + *ptr) == *ptr"\ +- Description: "Panic: |result| old(*ptr + *ptr) == *ptr"\ assertion\ - Status: SUCCESS\ -- Description: "|result| old(*ptr + *ptr + *ptr + *ptr) == *ptr"\ +- Description: "Panic: |result| old(*ptr + *ptr + *ptr + *ptr) == *ptr"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected index d9b0f5d51e5c..77975fe92b44 100644 --- a/tests/expected/function-contract/interior-mutability/api/cell.expected +++ b/tests/expected/function-contract/interior-mutability/api/cell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| im.x.get() < 101"\ +- Description: "Panic: |_| im.x.get() < 101"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected index b8da35411e53..1e942d0ee405 100644 --- a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected @@ -1,9 +1,9 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\ +- Description: "Panic: |_| old(im.x.get() + im.x.get()) == im.x.get()"\ assertion\ - Status: SUCCESS\ -- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\ +- Description: "Panic: |_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected index 1646a8a78e7f..88ca67f8f592 100644 --- a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected +++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| unsafe{ *im.x.get() } < 101"\ +- Description: "Panic: |_| unsafe{ *im.x.get() } < 101"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected index d9b0f5d51e5c..77975fe92b44 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected +++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| im.x.get() < 101"\ +- Description: "Panic: |_| im.x.get() < 101"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected index a367bcd9fb95..39549fb35f1c 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected +++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| im.x.get().is_some()"\ +- Description: "Panic: |_| im.x.get().is_some()"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected index 225c290a171e..beb6610d3644 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\ +- Description: "Panic: |_| unsafe{ *im.x.as_ptr() } < 101"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected index 1646a8a78e7f..88ca67f8f592 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected +++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| unsafe{ *im.x.get() } < 101"\ +- Description: "Panic: |_| unsafe{ *im.x.get() } < 101"\ in function modify VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.expected b/tests/expected/function-contract/modifies/expr_replace_fail.expected index f8019df2927c..5a085a6e6669 100644 --- a/tests/expected/function-contract/modifies/expr_replace_fail.expected +++ b/tests/expected/function-contract/modifies/expr_replace_fail.expected @@ -1,7 +1,7 @@ main.assertion\ - Status: FAILURE\ -- Description: ""Increment"" +- Description: "Panic: "Increment"" -Failed Checks: "Increment" +Failed Checks: Panic: "Increment" VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.expected b/tests/expected/function-contract/modifies/expr_replace_pass.expected index 405875334763..04692155438c 100644 --- a/tests/expected/function-contract/modifies/expr_replace_pass.expected +++ b/tests/expected/function-contract/modifies/expr_replace_pass.expected @@ -1,5 +1,5 @@ main.assertion\ - Status: SUCCESS\ -- Description: "Increment"\ +- Description: "Panic: Increment"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/field_replace_fail.expected b/tests/expected/function-contract/modifies/field_replace_fail.expected index 91643c68b3c5..d039019a2a64 100644 --- a/tests/expected/function-contract/modifies/field_replace_fail.expected +++ b/tests/expected/function-contract/modifies/field_replace_fail.expected @@ -1,7 +1,7 @@ main.assertion\ - Status: FAILURE\ -- Description: "Increment havocked" +- Description: "Panic: Increment havocked" -Failed Checks: Increment havocked +Failed Checks: Panic: Increment havocked VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/field_replace_pass.expected b/tests/expected/function-contract/modifies/field_replace_pass.expected index 64dedf3f511a..9849f195fe8f 100644 --- a/tests/expected/function-contract/modifies/field_replace_pass.expected +++ b/tests/expected/function-contract/modifies/field_replace_pass.expected @@ -1,9 +1,9 @@ main.assertion\ - Status: SUCCESS\ -- Description: "Increment"\ +- Description: "Panic: Increment"\ main.assertion\ - Status: SUCCESS\ -- Description: "Unchanged" +- Description: "Panic: Unchanged" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/global_replace_fail.expected b/tests/expected/function-contract/modifies/global_replace_fail.expected index 8c0761731a4b..ed3089f75fd9 100644 --- a/tests/expected/function-contract/modifies/global_replace_fail.expected +++ b/tests/expected/function-contract/modifies/global_replace_fail.expected @@ -1,8 +1,8 @@ main.assertion\ - Status: FAILURE\ -- Description: "not havocked"\ +- Description: "Panic: not havocked"\ in function main -Failed Checks: not havocked +Failed Checks: Panic: not havocked VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/global_replace_pass.expected b/tests/expected/function-contract/modifies/global_replace_pass.expected index 164f00c88d22..f55db1536346 100644 --- a/tests/expected/function-contract/modifies/global_replace_pass.expected +++ b/tests/expected/function-contract/modifies/global_replace_pass.expected @@ -1,6 +1,6 @@ main.assertion\ - Status: SUCCESS\ -- Description: "replaced"\ +- Description: "Panic: replaced"\ in function main VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected index f7bbb8202c46..7b9e6522d500 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.expected +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -1,6 +1,6 @@ .assertion\ - Status: SUCCESS\ -- Description: "equality"\ +- Description: "Panic: equality"\ in function copy_replace VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected index 7036111c76bf..ba4197c0c91b 100644 --- a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected @@ -1,6 +1,6 @@ copy_replace.assertion\ - Status: SUCCESS\ -- Description: "equality"\ +- Description: "Panic: equality"\ in function copy_replace VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.expected b/tests/expected/function-contract/modifies/mistake_condition_return.expected index ad1cbf4f72d2..b4fd83086339 100644 --- a/tests/expected/function-contract/modifies/mistake_condition_return.expected +++ b/tests/expected/function-contract/modifies/mistake_condition_return.expected @@ -1,3 +1,3 @@ -Failed Checks: assertion failed: res == 100 +Failed Checks: Panic: assertion failed: res == 100 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/unique_arguments.expected b/tests/expected/function-contract/modifies/unique_arguments.expected index d84097d648e9..5755fbc5acea 100644 --- a/tests/expected/function-contract/modifies/unique_arguments.expected +++ b/tests/expected/function-contract/modifies/unique_arguments.expected @@ -1,9 +1,9 @@ test_stubbing.assertion\ - Status: SUCCESS\ -- Description: "a is 1" +- Description: "Panic: a is 1" test_stubbing.assertion\ - Status: SUCCESS\ -- Description: "b is 2" +- Description: "Panic: b is 2" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected index 4ac03d025558..814d4fcd225d 100644 --- a/tests/expected/function-contract/modifies/vec_pass.expected +++ b/tests/expected/function-contract/modifies/vec_pass.expected @@ -1,20 +1,20 @@ .assertion\ - Status: SUCCESS\ -- Description: "v.len() > 0"\ +- Description: "Panic: v.len() > 0"\ in function modify .assertion\ - Status: SUCCESS\ -- Description: "element set"\ +- Description: "Panic: element set"\ in function modify .assertion\ - Status: SUCCESS\ -- Description: "vector tail equality"\ +- Description: "Panic: vector tail equality"\ in function modify assertion\ - Status: SUCCESS\ -- Description: "|result| v[0] == src" +- Description: "Panic: |result| v[0] == src" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected index 2fab679b5cba..e8211dee130a 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "Panic: |_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected index d0fc296ef4d7..6589e9a116d7 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x[0..3].iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "Panic: |_| x[0..3].iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected index 2fab679b5cba..e8211dee130a 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "Panic: |_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected index 2fab679b5cba..e8211dee130a 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "Panic: |_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/pattern_use.expected b/tests/expected/function-contract/pattern_use.expected index 1485191557db..be9a890c16b3 100644 --- a/tests/expected/function-contract/pattern_use.expected +++ b/tests/expected/function-contract/pattern_use.expected @@ -1,3 +1,3 @@ assertion\ - Status: FAILURE\ -- Description: "attempt to divide by zero"\ +- Description: "Panic: attempt to divide by zero"\ diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index 360242d07daf..33209a77750a 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "|result : &u32| *result == x"\ +- Description: "Panic: |result : &u32| *result == x"\ in function max -Failed Checks: |result : &u32| *result == x +Failed Checks: Panic: |result : &u32| *result == x VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index bdcde74c3bfe..a4673e3b0ddc 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|result : &u32| (*result == x) | (*result == y)"\ +- Description: "Panic: |result : &u32| (*result == x) | (*result == y)"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected index 0779b6dc88f8..9cbc7f474394 100644 --- a/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected +++ b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "|result| (*result == x) | (*result == y)"\ +- Description: "Panic: |result| (*result == x) | (*result == y)"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_replace_fail.expected b/tests/expected/function-contract/simple_replace_fail.expected index b6806befc22c..553bde62e9cd 100644 --- a/tests/expected/function-contract/simple_replace_fail.expected +++ b/tests/expected/function-contract/simple_replace_fail.expected @@ -1,3 +1,3 @@ main.assertion\ - Status: FAILURE\ -- Description: ""contract doesn't guarantee equality"" +- Description: "Panic: "contract doesn't guarantee equality"" diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected index 7dbc9bae68bd..4ca5bde3b2d1 100644 --- a/tests/expected/function-contract/simple_replace_pass.expected +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -1,9 +1,9 @@ .assertion\ - Status: SUCCESS\ -- Description: "divisor != 0" +- Description: "Panic: divisor != 0" main.assertion\ - Status: SUCCESS\ -- Description: ""contract guarantees smallness"" +- Description: "Panic: "contract guarantees smallness"" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/trait_impls/methods.expected b/tests/expected/function-contract/trait_impls/methods.expected index 3906a6fd7a10..3d5b34b53576 100644 --- a/tests/expected/function-contract/trait_impls/methods.expected +++ b/tests/expected/function-contract/trait_impls/methods.expected @@ -1,7 +1,7 @@ Checking harness check_next_y... Status: SUCCESS\ -Description: "|result| result.y == old(self.y) + 1"\ +Description: "Panic: |result| result.y == old(self.y) + 1"\ in function Point::next_y VERIFICATION:- SUCCESSFUL @@ -9,7 +9,7 @@ VERIFICATION:- SUCCESSFUL Checking harness check_add_x... Status: SUCCESS\ -Description: "|_| val < 0 || self.x >= old(self.x)"\ +Description: "Panic: |_| val < 0 || self.x >= old(self.x)"\ in function Point::add_x VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 38f31a63d5ca..82d1e7f0a4d7 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,10 +1,10 @@ Checking harness post_condition::harness... Failed Checks: Kani does not support reasoning about pointer to unallocated memory -Failed Checks: |result| kani::mem::can_dereference(result.0) +Failed Checks: Panic: |result| kani::mem::can_dereference(result.0) VERIFICATION:- FAILED Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20 +Failed Checks: Panic: assertion failed: unsafe { read_ptr(ptr) } == -20 Failed Checks: Kani does not support reasoning about pointer to unallocated memory Failed Checks: dereference failure: pointer outside object bounds VERIFICATION:- FAILED diff --git a/tests/expected/intrinsics/size_of_dst.expected b/tests/expected/intrinsics/size_of_dst.expected index 70fe457f9223..065f421ab55d 100644 --- a/tests/expected/intrinsics/size_of_dst.expected +++ b/tests/expected/intrinsics/size_of_dst.expected @@ -5,7 +5,7 @@ Status: FAILURE\ Description: "failed to compute `size_of_val`" Status: SUCCESS\ -Description: "assertion failed: unsafe { size_of_val_raw(new_ptr) } == expected_size" +Description: "Panic: assertion failed: unsafe { size_of_val_raw(new_ptr) } == expected_size" Failed Checks: failed to compute `size_of_val` VERIFICATION:- FAILED diff --git a/tests/expected/intrinsics/transmute_unchecked_size.expected b/tests/expected/intrinsics/transmute_unchecked_size.expected index 6ff9a1f67366..77b4359898ab 100644 --- a/tests/expected/intrinsics/transmute_unchecked_size.expected +++ b/tests/expected/intrinsics/transmute_unchecked_size.expected @@ -1,6 +1,6 @@ Checking harness transmute_wrapper_diff_size... Status: UNREACHABLE\ -Description: ""Unreachable expected"" +Description: "Panic: "Unreachable expected"" Failed Checks: Cannot transmute between types of different sizes. Transmuting from `8` to `16` bytes @@ -9,10 +9,10 @@ VERIFICATION:- FAILED Checking harness transmute_diff_size... Status: UNREACHABLE\ -Description: ""This should never be reached"" +Description: "Panic: "This should never be reached"" Status: UNREACHABLE\ -Description: ""Neither this one"" +Description: "Panic: "Neither this one"" Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `2` bytes Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `16` bytes diff --git a/tests/expected/issue-3022/issue_3022.expected b/tests/expected/issue-3022/issue_3022.expected index 9600182a5209..4fc10d3130ec 100644 --- a/tests/expected/issue-3022/issue_3022.expected +++ b/tests/expected/issue-3022/issue_3022.expected @@ -1,5 +1,5 @@ main.assertion\ - Status: SUCCESS\ -- Description: "assertion failed: inner == func2.inner" +- Description: "Panic: assertion failed: inner == func2.inner" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_with_prev_break_first_iter.expected b/tests/expected/loop-contract/loop_with_prev_break_first_iter.expected index 68dfcd51d085..0beaef7decbe 100644 --- a/tests/expected/loop-contract/loop_with_prev_break_first_iter.expected +++ b/tests/expected/loop-contract/loop_with_prev_break_first_iter.expected @@ -1,3 +1,3 @@ -Failed Checks: assertion failed: (i >= 2) && (i <= 100) && (__kani_prev_var_ +Failed Checks: Panic: assertion failed: (i >= 2) && (i <= 100) && (__kani_prev_var_ VERIFICATION:- FAILED diff --git a/tests/expected/loop-contract/struct_projection.expected b/tests/expected/loop-contract/struct_projection.expected index e398784ef656..ad28689a8384 100644 --- a/tests/expected/loop-contract/struct_projection.expected +++ b/tests/expected/loop-contract/struct_projection.expected @@ -8,7 +8,7 @@ struct_projection.loop_invariant_step.2\ struct_projection.assertion.3\ - Status: SUCCESS\ - - Description: "assertion failed: s.b == 2" + - Description: "Panic: assertion failed: s.b == 2" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/ptr_to_ref_cast/expected b/tests/expected/ptr_to_ref_cast/expected index 1b449911af11..bf4d51b250d6 100644 --- a/tests/expected/ptr_to_ref_cast/expected +++ b/tests/expected/ptr_to_ref_cast/expected @@ -61,7 +61,7 @@ Description: "dereference failure: pointer invalid"\ in function Store::<'_, 3>::from Status: SUCCESS\ -Description: "assertion failed: broken.data.len() == 3"\ +Description: "Panic: assertion failed: broken.data.len() == 3"\ in function check_store VERIFICATION:- FAILED @@ -72,4 +72,4 @@ Verification failed for - check_larger_deref_struct Verification failed for - check_larger_deref_into_ptr Verification failed for - check_larger_deref Verification failed for - check_store -Complete - 2 successfully verified harnesses, 5 failures, 7 total. \ No newline at end of file +Complete - 2 successfully verified harnesses, 5 failures, 7 total. diff --git a/tests/expected/raw_slice/expected b/tests/expected/raw_slice/expected index d2bd2b505ef7..61a4479825eb 100644 --- a/tests/expected/raw_slice/expected +++ b/tests/expected/raw_slice/expected @@ -1,15 +1,15 @@ Checking harness check_non_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 4"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 4"\ slice.rs:61:5 in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 4"\ +Description: "Panic: assertion failed: raw.inner.len() == 4"\ slice.rs:62:5 in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner[0] == 1"\ +Description: "Panic: assertion failed: raw.inner[0] == 1"\ slice.rs:63:5 in function check_non_empty_raw VERIFICATION:- SUCCESSFUL @@ -17,11 +17,11 @@ VERIFICATION:- SUCCESSFUL Checking harness check_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 0"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 0"\ slice.rs:70:5 in function check_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 0"\ +Description: "Panic: assertion failed: raw.inner.len() == 0"\ slice.rs:71:5 in function check_empty_raw VERIFICATION:- SUCCESSFUL @@ -29,19 +29,19 @@ VERIFICATION:- SUCCESSFUL Checking harness check_non_empty_slice... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(slice) == 2"\ +Description: "Panic: assertion failed: mem::size_of_val(slice) == 2"\ slice.rs:78:5 in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others.len() == 1"\ +Description: "Panic: assertion failed: slice.others.len() == 1"\ slice.rs:79:5 in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.first == 1"\ +Description: "Panic: assertion failed: slice.first == 1"\ slice.rs:80:5 in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == 5"\ +Description: "Panic: assertion failed: slice.others[0] == 5"\ slice.rs:81:5 in function check_non_empty_slice VERIFICATION:- SUCCESSFUL @@ -50,15 +50,15 @@ VERIFICATION:- SUCCESSFUL Checking harness check_naive_iterator_should_fail... Status: SUCCESS\ -Description: ""Naive new should have the wrong slice len""\ +Description: "Panic: "Naive new should have the wrong slice len""\ slice.rs:94:5 in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.first == first"\ +Description: "Panic: assertion failed: slice.first == first"\ slice.rs:95:5 in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == second"\ +Description: "Panic: assertion failed: slice.others[0] == second"\ slice.rs:96:5 in function check_naive_iterator_should_fail Status: FAILURE\ diff --git a/tests/expected/raw_slice_c_repr/expected b/tests/expected/raw_slice_c_repr/expected index d0097ffc1349..14885ee633a5 100644 --- a/tests/expected/raw_slice_c_repr/expected +++ b/tests/expected/raw_slice_c_repr/expected @@ -1,15 +1,15 @@ Checking harness check_non_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 4"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 4"\ in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 4"\ +Description: "Panic: assertion failed: raw.inner.len() == 4"\ in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner[0] == 1"\ +Description: "Panic: assertion failed: raw.inner[0] == 1"\ in function check_non_empty_raw VERIFICATION:- SUCCESSFUL @@ -17,11 +17,11 @@ VERIFICATION:- SUCCESSFUL Checking harness check_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 0"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 0"\ in function check_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 0"\ +Description: "Panic: assertion failed: raw.inner.len() == 0"\ in function check_empty_raw VERIFICATION:- SUCCESSFUL @@ -29,19 +29,19 @@ VERIFICATION:- SUCCESSFUL Checking harness check_non_empty_slice... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(slice) == 2"\ +Description: "Panic: assertion failed: mem::size_of_val(slice) == 2"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others.len() == 1"\ +Description: "Panic: assertion failed: slice.others.len() == 1"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.first == 1"\ +Description: "Panic: assertion failed: slice.first == 1"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == 5"\ +Description: "Panic: assertion failed: slice.others[0] == 5"\ in function check_non_empty_slice VERIFICATION:- SUCCESSFUL @@ -50,15 +50,15 @@ VERIFICATION:- SUCCESSFUL Checking harness check_naive_iterator_should_fail... Status: SUCCESS\ -Description: ""Naive new should have the wrong slice len""\ +Description: "Panic: "Naive new should have the wrong slice len""\ in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.first == first"\ +Description: "Panic: assertion failed: slice.first == first"\ in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == second"\ +Description: "Panic: assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ diff --git a/tests/expected/raw_slice_packed/expected b/tests/expected/raw_slice_packed/expected index d0097ffc1349..14885ee633a5 100644 --- a/tests/expected/raw_slice_packed/expected +++ b/tests/expected/raw_slice_packed/expected @@ -1,15 +1,15 @@ Checking harness check_non_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 4"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 4"\ in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 4"\ +Description: "Panic: assertion failed: raw.inner.len() == 4"\ in function check_non_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner[0] == 1"\ +Description: "Panic: assertion failed: raw.inner[0] == 1"\ in function check_non_empty_raw VERIFICATION:- SUCCESSFUL @@ -17,11 +17,11 @@ VERIFICATION:- SUCCESSFUL Checking harness check_empty_raw... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(raw) == 0"\ +Description: "Panic: assertion failed: mem::size_of_val(raw) == 0"\ in function check_empty_raw Status: SUCCESS\ -Description: "assertion failed: raw.inner.len() == 0"\ +Description: "Panic: assertion failed: raw.inner.len() == 0"\ in function check_empty_raw VERIFICATION:- SUCCESSFUL @@ -29,19 +29,19 @@ VERIFICATION:- SUCCESSFUL Checking harness check_non_empty_slice... Status: SUCCESS\ -Description: "assertion failed: mem::size_of_val(slice) == 2"\ +Description: "Panic: assertion failed: mem::size_of_val(slice) == 2"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others.len() == 1"\ +Description: "Panic: assertion failed: slice.others.len() == 1"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.first == 1"\ +Description: "Panic: assertion failed: slice.first == 1"\ in function check_non_empty_slice Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == 5"\ +Description: "Panic: assertion failed: slice.others[0] == 5"\ in function check_non_empty_slice VERIFICATION:- SUCCESSFUL @@ -50,15 +50,15 @@ VERIFICATION:- SUCCESSFUL Checking harness check_naive_iterator_should_fail... Status: SUCCESS\ -Description: ""Naive new should have the wrong slice len""\ +Description: "Panic: "Naive new should have the wrong slice len""\ in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.first == first"\ +Description: "Panic: assertion failed: slice.first == first"\ in function check_naive_iterator_should_fail Status: SUCCESS\ -Description: "assertion failed: slice.others[0] == second"\ +Description: "Panic: assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ diff --git a/tests/expected/reach/assert/reachable_fail/expected b/tests/expected/reach/assert/reachable_fail/expected index 9232a6752fa9..156f252d071e 100644 --- a/tests/expected/reach/assert/reachable_fail/expected +++ b/tests/expected/reach/assert/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "assertion failed: x != 5" -Failed Checks: assertion failed: x != 5 +Description: "Panic: assertion failed: x != 5" +Failed Checks: Panic: assertion failed: x != 5 diff --git a/tests/expected/reach/assert/reachable_pass/expected b/tests/expected/reach/assert/reachable_pass/expected index 8095cccc7e7b..7a19097b3383 100644 --- a/tests/expected/reach/assert/reachable_pass/expected +++ b/tests/expected/reach/assert/reachable_pass/expected @@ -1,3 +1,3 @@ SUCCESS\ -Description: "assertion failed: x > 4" +Description: "Panic: assertion failed: x > 4" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/reach/assert/unreachable/expected b/tests/expected/reach/assert/unreachable/expected index e8129d3fcf4f..aa5885c0d6c3 100644 --- a/tests/expected/reach/assert/unreachable/expected +++ b/tests/expected/reach/assert/unreachable/expected @@ -1,3 +1,3 @@ UNREACHABLE\ -Description: "assertion failed: x == 2" +Description: "Panic: assertion failed: x == 2" ** 1 of 3 failed (1 unreachable) diff --git a/tests/expected/reach/assert_eq/unreachable/expected b/tests/expected/reach/assert_eq/unreachable/expected index d5308a559088..96ce777af623 100644 --- a/tests/expected/reach/assert_eq/unreachable/expected +++ b/tests/expected/reach/assert_eq/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: y == 55" +Description: "Panic: assertion failed: y == 55" diff --git a/tests/expected/reach/assert_ne/unreachable/expected b/tests/expected/reach/assert_ne/unreachable/expected index 2a54a183fa1a..a4bacf74d6cd 100644 --- a/tests/expected/reach/assert_ne/unreachable/expected +++ b/tests/expected/reach/assert_ne/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: y != 1" +Description: "Panic: assertion failed: y != 1" diff --git a/tests/expected/reach/bounds/reachable_fail/expected b/tests/expected/reach/bounds/reachable_fail/expected index c2af72512030..0e27fc6d6895 100644 --- a/tests/expected/reach/bounds/reachable_fail/expected +++ b/tests/expected/reach/bounds/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "index out of bounds: the length is less than or equal to the given index" -Failed Checks: index out of bounds: the length is less than or equal to the given index +Description: "Panic: index out of bounds: the length is less than or equal to the given index" +Failed Checks: Panic: index out of bounds: the length is less than or equal to the given index diff --git a/tests/expected/reach/bounds/reachable_pass/expected b/tests/expected/reach/bounds/reachable_pass/expected index bb362be692cb..77d1aa33957f 100644 --- a/tests/expected/reach/bounds/reachable_pass/expected +++ b/tests/expected/reach/bounds/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "index out of bounds: the length is less than or equal to the given index" +Description: "Panic: index out of bounds: the length is less than or equal to the given index" diff --git a/tests/expected/reach/bounds/unreachable/expected b/tests/expected/reach/bounds/unreachable/expected index feff42f37752..513f2cb84d7c 100644 --- a/tests/expected/reach/bounds/unreachable/expected +++ b/tests/expected/reach/bounds/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "index out of bounds: the length is less than or equal to the given index" +Description: "Panic: index out of bounds: the length is less than or equal to the given index" diff --git a/tests/expected/reach/check_id/expected b/tests/expected/reach/check_id/expected index 70db7c27769b..ff879a5beb8c 100644 --- a/tests/expected/reach/check_id/expected +++ b/tests/expected/reach/check_id/expected @@ -1,10 +1,10 @@ Status: FAILURE\ -Description: "assertion failed: 3 + 3 == 5" +Description: "Panic: assertion failed: 3 + 3 == 5" Status: UNREACHABLE\ -Description: "assertion failed: 2 + 2 == 4" +Description: "Panic: assertion failed: 2 + 2 == 4" Status: SUCCESS\ -Description: "assertion failed: 1 + 1 == 2" +Description: "Panic: assertion failed: 1 + 1 == 2" VERIFICATION:- FAILED diff --git a/tests/expected/reach/debug-assert-eq/reachable_fail/expected b/tests/expected/reach/debug-assert-eq/reachable_fail/expected index 6509b9fd31ff..87deff5f4a2b 100644 --- a/tests/expected/reach/debug-assert-eq/reachable_fail/expected +++ b/tests/expected/reach/debug-assert-eq/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "assertion failed: x == 10" -Failed Checks: assertion failed: x == 10 +Description: "Panic: assertion failed: x == 10" +Failed Checks: Panic: assertion failed: x == 10 diff --git a/tests/expected/reach/debug-assert-eq/reachable_pass/expected b/tests/expected/reach/debug-assert-eq/reachable_pass/expected index 262971305413..983e30661162 100644 --- a/tests/expected/reach/debug-assert-eq/reachable_pass/expected +++ b/tests/expected/reach/debug-assert-eq/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "assertion failed: x == 10" +Description: "Panic: assertion failed: x == 10" diff --git a/tests/expected/reach/debug-assert-eq/unreachable/expected b/tests/expected/reach/debug-assert-eq/unreachable/expected index 097f270f3234..3d50909651c6 100644 --- a/tests/expected/reach/debug-assert-eq/unreachable/expected +++ b/tests/expected/reach/debug-assert-eq/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: x == 10" +Description: "Panic: assertion failed: x == 10" diff --git a/tests/expected/reach/debug-assert-ne/reachable_fail/expected b/tests/expected/reach/debug-assert-ne/reachable_fail/expected index ac52bb2fec87..20637900a6db 100644 --- a/tests/expected/reach/debug-assert-ne/reachable_fail/expected +++ b/tests/expected/reach/debug-assert-ne/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "assertion failed: x != 17" -Failed Checks: assertion failed: x != 17 +Description: "Panic: assertion failed: x != 17" +Failed Checks: Panic: assertion failed: x != 17 diff --git a/tests/expected/reach/debug-assert-ne/reachable_pass/expected b/tests/expected/reach/debug-assert-ne/reachable_pass/expected index b75c6cfe4806..784e6b77bab0 100644 --- a/tests/expected/reach/debug-assert-ne/reachable_pass/expected +++ b/tests/expected/reach/debug-assert-ne/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "assertion failed: x != 17" +Description: "Panic: assertion failed: x != 17" diff --git a/tests/expected/reach/debug-assert-ne/unreachable/expected b/tests/expected/reach/debug-assert-ne/unreachable/expected index 343ae2617fcd..3fbaa117ae8f 100644 --- a/tests/expected/reach/debug-assert-ne/unreachable/expected +++ b/tests/expected/reach/debug-assert-ne/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: x != 17" +Description: "Panic: assertion failed: x != 17" diff --git a/tests/expected/reach/debug-assert/reachable_fail/expected b/tests/expected/reach/debug-assert/reachable_fail/expected index 18b0b00d7783..0e076632f919 100644 --- a/tests/expected/reach/debug-assert/reachable_fail/expected +++ b/tests/expected/reach/debug-assert/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "assertion failed: x != -10" -Failed Checks: assertion failed: x != -10 +Description: "Panic: assertion failed: x != -10" +Failed Checks: Panic: assertion failed: x != -10 diff --git a/tests/expected/reach/debug-assert/reachable_pass/expected b/tests/expected/reach/debug-assert/reachable_pass/expected index 0b34ddf6e3bb..e799ee85007f 100644 --- a/tests/expected/reach/debug-assert/reachable_pass/expected +++ b/tests/expected/reach/debug-assert/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "assertion failed: x != -10" +Description: "Panic: assertion failed: x != -10" diff --git a/tests/expected/reach/debug-assert/unreachable/expected b/tests/expected/reach/debug-assert/unreachable/expected index 23e51e949654..b24fa83b0a52 100644 --- a/tests/expected/reach/debug-assert/unreachable/expected +++ b/tests/expected/reach/debug-assert/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "assertion failed: x != -10" +Description: "Panic: assertion failed: x != -10" diff --git a/tests/expected/reach/div-zero/reachable_fail/expected b/tests/expected/reach/div-zero/reachable_fail/expected index 047ab8906e02..c08efefb58ed 100644 --- a/tests/expected/reach/div-zero/reachable_fail/expected +++ b/tests/expected/reach/div-zero/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "attempt to divide by zero" -Failed Checks: attempt to divide by zero +Description: "Panic: attempt to divide by zero" +Failed Checks: Panic: attempt to divide by zero diff --git a/tests/expected/reach/div-zero/unreachable/expected b/tests/expected/reach/div-zero/unreachable/expected index 99c623fd211b..9bd0c5afb079 100644 --- a/tests/expected/reach/div-zero/unreachable/expected +++ b/tests/expected/reach/div-zero/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "attempt to divide by zero" +Description: "Panic: attempt to divide by zero" diff --git a/tests/expected/reach/overflow-neg/reachable_fail/expected b/tests/expected/reach/overflow-neg/reachable_fail/expected index ecdccd43f35d..81df7ec711d7 100644 --- a/tests/expected/reach/overflow-neg/reachable_fail/expected +++ b/tests/expected/reach/overflow-neg/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "attempt to negate with overflow" -Failed Checks: attempt to negate with overflow +Description: "Panic: attempt to negate with overflow" +Failed Checks: Panic: attempt to negate with overflow diff --git a/tests/expected/reach/overflow-neg/reachable_pass/expected b/tests/expected/reach/overflow-neg/reachable_pass/expected index 10e2d12e1e67..e8cfa7c64ff3 100644 --- a/tests/expected/reach/overflow-neg/reachable_pass/expected +++ b/tests/expected/reach/overflow-neg/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "attempt to negate with overflow" +Description: "Panic: attempt to negate with overflow" diff --git a/tests/expected/reach/overflow-neg/unreachable/expected b/tests/expected/reach/overflow-neg/unreachable/expected index cf2bd4d96f57..57ae1ee851d8 100644 --- a/tests/expected/reach/overflow-neg/unreachable/expected +++ b/tests/expected/reach/overflow-neg/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "attempt to negate with overflow" +Description: "Panic: attempt to negate with overflow" diff --git a/tests/expected/reach/overflow/reachable_fail/expected b/tests/expected/reach/overflow/reachable_fail/expected index ea7b2089301b..d6274052115d 100644 --- a/tests/expected/reach/overflow/reachable_fail/expected +++ b/tests/expected/reach/overflow/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "attempt to subtract with overflow" -Failed Checks: attempt to subtract with overflow +Description: "Panic: attempt to subtract with overflow" +Failed Checks: Panic: attempt to subtract with overflow diff --git a/tests/expected/reach/overflow/reachable_pass/expected b/tests/expected/reach/overflow/reachable_pass/expected index 3046e859a1f1..02ee98098e86 100644 --- a/tests/expected/reach/overflow/reachable_pass/expected +++ b/tests/expected/reach/overflow/reachable_pass/expected @@ -1,2 +1,2 @@ SUCCESS\ -Description: "attempt to subtract with overflow" +Description: "Panic: attempt to subtract with overflow" diff --git a/tests/expected/reach/overflow/unreachable/expected b/tests/expected/reach/overflow/unreachable/expected index 379b0fb068f8..59d0b110457b 100644 --- a/tests/expected/reach/overflow/unreachable/expected +++ b/tests/expected/reach/overflow/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "attempt to subtract with overflow" +Description: "Panic: attempt to subtract with overflow" diff --git a/tests/expected/reach/rem-zero/reachable_fail/expected b/tests/expected/reach/rem-zero/reachable_fail/expected index d01a76e4a69c..d41ffe1177ff 100644 --- a/tests/expected/reach/rem-zero/reachable_fail/expected +++ b/tests/expected/reach/rem-zero/reachable_fail/expected @@ -1,3 +1,3 @@ FAILURE\ -Description: "attempt to calculate the remainder with a divisor of zero" -Failed Checks: attempt to calculate the remainder with a divisor of zero +Description: "Panic: attempt to calculate the remainder with a divisor of zero" +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero diff --git a/tests/expected/reach/rem-zero/unreachable/expected b/tests/expected/reach/rem-zero/unreachable/expected index 1a906cd13651..91518a8b92fe 100644 --- a/tests/expected/reach/rem-zero/unreachable/expected +++ b/tests/expected/reach/rem-zero/unreachable/expected @@ -1,2 +1,2 @@ UNREACHABLE\ -Description: "attempt to calculate the remainder with a divisor of zero" +Description: "Panic: attempt to calculate the remainder with a divisor of zero" diff --git a/tests/expected/report/insufficient_unwind/expected b/tests/expected/report/insufficient_unwind/expected index c7f83da7b3ac..a685d847064c 100644 --- a/tests/expected/report/insufficient_unwind/expected +++ b/tests/expected/report/insufficient_unwind/expected @@ -1,4 +1,4 @@ UNDETERMINED\ -Description: "assertion failed: sum == 6" +Description: "Panic: assertion failed: sum == 6" [Kani] info: Verification output shows one or more unwinding failures. [Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. diff --git a/tests/expected/report/uncolor/expected b/tests/expected/report/uncolor/expected index 435fbf43ab97..65d352aa2116 100644 --- a/tests/expected/report/uncolor/expected +++ b/tests/expected/report/uncolor/expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ -Description: "assertion failed: 1 + 1 == 2" +Description: "Panic: assertion failed: 1 + 1 == 2" - Status: FAILURE\ -- Description: "assertion failed: 2 + 2 == 3" +- Description: "Panic: assertion failed: 2 + 2 == 3" VERIFICATION:- FAILED diff --git a/tests/expected/report/unsupported/failure/expected b/tests/expected/report/unsupported/failure/expected index 1e8d7e64994a..08ba2b86a20f 100644 --- a/tests/expected/report/unsupported/failure/expected +++ b/tests/expected/report/unsupported/failure/expected @@ -1,5 +1,5 @@ FAILURE\ -Description: "assertion failed: x == 0" -Failed Checks: assertion failed: x == 0 +Description: "Panic: assertion failed: x == 0" +Failed Checks: Panic: assertion failed: x == 0 Failed Checks: TerminatorKind::InlineAsm is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2 ** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details. diff --git a/tests/expected/report/unsupported/reachable/expected b/tests/expected/report/unsupported/reachable/expected index afa43c9be605..69865c8b4e31 100644 --- a/tests/expected/report/unsupported/reachable/expected +++ b/tests/expected/report/unsupported/reachable/expected @@ -1,4 +1,4 @@ Status: UNDETERMINED\ -Description: "assertion failed: x == 0" +Description: "Panic: assertion failed: x == 0" Failed Checks: TerminatorKind::InlineAsm is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2 ** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details. diff --git a/tests/expected/report/unsupported/unreachable/expected b/tests/expected/report/unsupported/unreachable/expected index c99f6c708acf..26d58176f6fd 100644 --- a/tests/expected/report/unsupported/unreachable/expected +++ b/tests/expected/report/unsupported/unreachable/expected @@ -1,3 +1,3 @@ SUCCESS\ -Description: "assertion failed: x == 0" +Description: "Panic: assertion failed: x == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/safety-constraint-attribute/abstract-value/expected b/tests/expected/safety-constraint-attribute/abstract-value/expected index 2fc76378041d..6570ab964214 100644 --- a/tests/expected/safety-constraint-attribute/abstract-value/expected +++ b/tests/expected/safety-constraint-attribute/abstract-value/expected @@ -1,6 +1,6 @@ Check 1: check_abstract_value.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: value.is_safe()" + - Description: "Panic: assertion failed: value.is_safe()" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/expected b/tests/expected/safety-constraint-attribute/check-arbitrary/expected index ee1e13bb726d..597d681706a2 100644 --- a/tests/expected/safety-constraint-attribute/check-arbitrary/expected +++ b/tests/expected/safety-constraint-attribute/check-arbitrary/expected @@ -1,11 +1,11 @@ Check 1: check_arbitrary.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: point.x >= 0" + - Description: "Panic: assertion failed: point.x >= 0" Check 2: check_arbitrary.assertion.2\ - Status: SUCCESS\ - - Description: "assertion failed: point.y >= 0" + - Description: "Panic: assertion failed: point.y >= 0" Check 3: check_arbitrary.assertion.3\ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "Panic: assertion failed: point.is_safe()" diff --git a/tests/expected/safety-constraint-attribute/check-invariant/expected b/tests/expected/safety-constraint-attribute/check-invariant/expected index a4605f03b7b4..3cce288b9a93 100644 --- a/tests/expected/safety-constraint-attribute/check-invariant/expected +++ b/tests/expected/safety-constraint-attribute/check-invariant/expected @@ -1,7 +1,7 @@ Check 1: check_invariant.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "Panic: assertion failed: point.is_safe()" Check 2: check_invariant.assertion.2\ - Status: UNREACHABLE\ - - Description: ""this assertion should be unreachable"" + - Description: "Panic: "this assertion should be unreachable"" diff --git a/tests/expected/safety-constraint-attribute/grade-example/expected b/tests/expected/safety-constraint-attribute/grade-example/expected index fd95a713d65a..311a276c4032 100644 --- a/tests/expected/safety-constraint-attribute/grade-example/expected +++ b/tests/expected/safety-constraint-attribute/grade-example/expected @@ -1,10 +1,10 @@ Grade::check_percentage_safety.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: self.percentage <= 100" + - Description: "Panic: assertion failed: self.percentage <= 100" check_grade_safe.assertion.1\ - Status: SUCCESS\ - - Description: "assertion failed: grade.is_safe()" + - Description: "Panic: assertion failed: grade.is_safe()" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/shadow/uninit_array/expected b/tests/expected/shadow/uninit_array/expected index 1d5f70698010..924a6a03e809 100644 --- a/tests/expected/shadow/uninit_array/expected +++ b/tests/expected/shadow/uninit_array/expected @@ -1,3 +1,3 @@ -Failed Checks: assertion failed: SM.get(p) +Failed Checks: Panic: assertion failed: SM.get(p) Verification failed for - check_init_any Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/unsupported_num_objects/expected b/tests/expected/shadow/unsupported_num_objects/expected index da3b5a671969..386e96a78ce8 100644 --- a/tests/expected/shadow/unsupported_num_objects/expected +++ b/tests/expected/shadow/unsupported_num_objects/expected @@ -1,3 +1,3 @@ -Failed Checks: The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024) +Failed Checks: Panic: The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024) Verification failed for - check_max_objects_fail Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/shadow/unsupported_object_size/expected b/tests/expected/shadow/unsupported_object_size/expected index a4598b5aac82..0d03f54bdbb5 100644 --- a/tests/expected/shadow/unsupported_object_size/expected +++ b/tests/expected/shadow/unsupported_object_size/expected @@ -1,3 +1,3 @@ -Failed Checks: The object size exceeds the maximum size supported by Kani's shadow memory model (64) +Failed Checks: Panic: The object size exceeds the maximum size supported by Kani's shadow memory model (64) Verification failed for - check_max_object_size_fail Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/trait-receiver/expected b/tests/expected/trait-receiver/expected index 6a6314b650cb..6fc54f877cb4 100644 --- a/tests/expected/trait-receiver/expected +++ b/tests/expected/trait-receiver/expected @@ -1,16 +1,16 @@ Checking harness check_box... Status: SUCCESS\ -Description: "assertion failed: boxed.ref_id() == id"\ +Description: "Panic: assertion failed: boxed.ref_id() == id"\ in function check_box Status: SUCCESS\ -Description: "assertion failed: boxed.box_id() == id"\ +Description: "Panic: assertion failed: boxed.box_id() == id"\ in function check_box Status: SUCCESS\ -Description: "assertion failed: self.as_ref().id == self.id"\ +Description: "Panic: assertion failed: self.as_ref().id == self.id"\ in function ::box_id VERIFICATION:- SUCCESSFUL @@ -19,16 +19,16 @@ VERIFICATION:- SUCCESSFUL Checking harness check_rc... Status: SUCCESS\ -Description: "assertion failed: ref_count.ref_id() == id"\ +Description: "Panic: assertion failed: ref_count.ref_id() == id"\ in function check_rc Status: SUCCESS\ -Description: "assertion failed: ref_count.rc_id() == id"\ +Description: "Panic: assertion failed: ref_count.rc_id() == id"\ in function check_rc Status: SUCCESS\ -Description: "assertion failed: self.as_ref().id == self.id"\ +Description: "Panic: assertion failed: self.as_ref().id == self.id"\ in function ::rc_id VERIFICATION:- SUCCESSFUL @@ -37,16 +37,16 @@ VERIFICATION:- SUCCESSFUL Checking harness check_arc... Status: SUCCESS\ -Description: "assertion failed: async_ref.ref_id() == id"\ +Description: "Panic: assertion failed: async_ref.ref_id() == id"\ in function check_arc Status: SUCCESS\ -Description: "assertion failed: async_ref.arc_id() == id"\ +Description: "Panic: assertion failed: async_ref.arc_id() == id"\ in function check_arc Status: SUCCESS\ -Description: "assertion failed: self.as_ref().id == self.id"\ +Description: "Panic: assertion failed: self.as_ref().id == self.id"\ in function ::arc_id VERIFICATION:- SUCCESSFUL @@ -55,15 +55,15 @@ VERIFICATION:- SUCCESSFUL Checking harness check_pin... Status: SUCCESS\ -Description: "assertion failed: pin.ref_id() == id"\ +Description: "Panic: assertion failed: pin.ref_id() == id"\ in function check_pin Status: SUCCESS\ -Description: "assertion failed: pin.pin_id() == id"\ +Description: "Panic: assertion failed: pin.pin_id() == id"\ in function check_pin Status: SUCCESS\ -Description: "assertion failed: self.as_ref().id == self.id"\ +Description: "Panic: assertion failed: self.as_ref().id == self.id"\ in function ::pin_id @@ -72,15 +72,15 @@ VERIFICATION:- SUCCESSFUL Checking harness check_pin_box... Status: SUCCESS\ -Description: "assertion failed: pin.ref_id() == id"\ +Description: "Panic: assertion failed: pin.ref_id() == id"\ in function check_pin_box Status: SUCCESS\ -Description: "assertion failed: pin.pin_box_id() == id"\ +Description: "Panic: assertion failed: pin.pin_box_id() == id"\ in function check_pin_box Status: SUCCESS\ -Description: "assertion failed: self.as_ref().id == self.id"\ +Description: "Panic: assertion failed: self.as_ref().id == self.id"\ in function ::pin_box_id VERIFICATION:- SUCCESSFUL @@ -89,11 +89,11 @@ VERIFICATION:- SUCCESSFUL Checking harness check_mut... Status: SUCCESS\ -Description: "assertion failed: trt.replace_id(new_id) == initial_id"\ +Description: "Panic: assertion failed: trt.replace_id(new_id) == initial_id"\ in function check_mut Status: SUCCESS\ -Description: "assertion failed: trt.ref_id() == new_id"\ +Description: "Panic: assertion failed: trt.ref_id() == new_id"\ in function check_mut VERIFICATION:- SUCCESSFUL @@ -102,7 +102,7 @@ VERIFICATION:- SUCCESSFUL Checking harness check_bound... Status: SUCCESS\ -Description: "assertion failed: obj.bound_value() == id"\ +Description: "Panic: assertion failed: obj.bound_value() == id"\ in function check_bound::assert_value:: VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/valid-value-checks/char_validity.expected b/tests/expected/valid-value-checks/char_validity.expected index 28c0d6d06e79..b69f4ed4a3a8 100644 --- a/tests/expected/valid-value-checks/char_validity.expected +++ b/tests/expected/valid-value-checks/char_validity.expected @@ -1,19 +1,19 @@ Checking harness check_invalid_char_unit_wrapper_should_fail... - Status: UNREACHABLE\ -- Description: ""Unreachable code: Expected invalid char wrapper detection"" +- Description: "Panic: "Unreachable code: Expected invalid char wrapper detection"" Failed Checks: Undefined Behavior: Invalid value of type `TwoFields` Failed Checks: Undefined Behavior: Invalid value of type `TwoFields<(), char>` VERIFICATION:- FAILED Checking harness check_invalid_char_nonzero_wrapper_should_fail... - Status: UNREACHABLE\ -- Description: ""Unreachable code: Expected invalid char / NonZero detection"" +- Description: "Panic: "Unreachable code: Expected invalid char / NonZero detection"" Failed Checks: Undefined Behavior: Invalid value of type `TwoFields>` VERIFICATION:- FAILED Checking harness check_invalid_char_should_fail... - Status: UNREACHABLE\ -- Description: ""Unreachable code: Expected invalid char detection"" +- Description: "Panic: "Unreachable code: Expected invalid char detection"" Failed Checks: Undefined Behavior: Invalid value of type `char` VERIFICATION:- FAILED diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index 2afedc9e0b0a..8bfd78c99c01 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -21,17 +21,17 @@ Skipped Functions: None. Kani generated automatic harnesses for all functions in Autoharness: Checking function should_fail::max's contract against all possible inputs... assertion\ - Status: FAILURE\ - - Description: "|result : &u32| *result == x" + - Description: "Panic: |result : &u32| *result == x" Autoharness: Checking function should_pass::has_loop_contract against all possible inputs... should_pass::has_loop_contract.assertion\ - Status: SUCCESS\ - - Description: "assertion failed: x == 2" + - Description: "Panic: assertion failed: x == 2" Autoharness: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... assertion\ - Status: SUCCESS\ - - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" + - Description: "Panic: |result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" Autoharness: Checking function should_pass::div's contract against all possible inputs... @@ -48,7 +48,7 @@ should_pass::alignment::Alignment::as_usize\ should_pass::alignment::Alignment::as_usize\ - Status: SUCCESS\ - - Description: "|result| result.is_power_of_two()" + - Description: "Panic: |result| result.is_power_of_two()" Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected index b139d5777928..6f8939a7d122 100644 --- a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected @@ -23,7 +23,7 @@ panic.assertion\ Autoharness: Checking function integer_overflow against all possible inputs... assertion\ - Status: FAILURE - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" Autoharness: Checking function oob_unsafe_array_access against all possible inputs... oob_unsafe_array_access.pointer_dereference\ @@ -33,7 +33,7 @@ oob_unsafe_array_access.pointer_dereference\ Autoharness: Checking function oob_safe_array_access against all possible inputs... assertion\ - Status: FAILURE\ - - Description: "index out of bounds: the length is less than or equal to the given index" + - Description: "Panic: index out of bounds: the length is less than or equal to the given index" Autoharness: Checking function unchecked_mul against all possible inputs... arithmetic_overflow\ @@ -48,7 +48,7 @@ panic.assertion\ Checking harness integer_overflow_harness... assertion\ - Status: FAILURE\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" Checking harness oob_unsafe_array_access_harness... oob_unsafe_array_access.pointer_dereference\ @@ -57,7 +57,7 @@ oob_unsafe_array_access.pointer_dereference\ Checking harness oob_safe_array_access_harness... assertion\ - Status: FAILURE\ - - Description: "index out of bounds: the length is less than or equal to the given index" + - Description: "Panic: index out of bounds: the length is less than or equal to the given index" Checking harness unchecked_mul_harness... arithmetic_overflow\ diff --git a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.expected b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.expected index 6d0c229e436a..94b4b63c312a 100644 --- a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.expected +++ b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.expected @@ -13,7 +13,7 @@ Not unwinding recursion gcd_recursion iteration 21 gcd_recursion.assertion\ - Status: FAILURE\ - - Description: "attempt to calculate the remainder with a divisor of zero" + - Description: "Panic: attempt to calculate the remainder with a divisor of zero" gcd_recursion.recursion\ - Status: FAILURE\ diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected index cc8e9b32ca14..00979072f8c7 100644 --- a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected @@ -20,71 +20,71 @@ Kani generated automatic harnesses for 7 function(s): Autoharness: Checking function Nanoseconds::new_unchecked's contract against all possible inputs... Nanoseconds::new_unchecked\ - Status: SUCCESS\ - - Description: "|nano| nano.is_safe()" + - Description: "Panic: |nano| nano.is_safe()" Autoharness: Checking function Duration::checked_sub's contract against all possible inputs... Duration::checked_sub\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" Duration::checked_sub\ - Status: SUCCESS\ - - Description: "attempt to subtract with overflow" + - Description: "Panic: attempt to subtract with overflow" Nanoseconds::new_unchecked\ - Status: SUCCESS\ - - Description: "val < NANOS_PER_SEC" + - Description: "Panic: val < NANOS_PER_SEC" Duration::checked_sub\ - Status: SUCCESS\ - - Description: "|duration| duration.is_none() || duration.unwrap().is_safe()" + - Description: "Panic: |duration| duration.is_none() || duration.unwrap().is_safe()" Duration::new\ - Status: SUCCESS\ - - Description: "|duration| duration.is_safe()" + - Description: "Panic: |duration| duration.is_safe()" Autoharness: Checking function Duration::checked_add's contract against all possible inputs... Nanoseconds::new_unchecked\ - Status: SUCCESS\ - - Description: "val < NANOS_PER_SEC" + - Description: "Panic: val < NANOS_PER_SEC" Duration::new\ - Status: SUCCESS\ - - Description: "|duration| duration.is_safe()" + - Description: "Panic: |duration| duration.is_safe()" Duration::checked_add\ - Status: SUCCESS\ - - Description: "|duration| duration.is_none() || duration.unwrap().is_safe()" + - Description: "Panic: |duration| duration.is_none() || duration.unwrap().is_safe()" Duration::checked_add\ - Status: SUCCESS\ - - Description: "attempt to add with overflow" + - Description: "Panic: attempt to add with overflow" Duration::checked_add\ - Status: SUCCESS\ - - Description: "attempt to subtract with overflow" + - Description: "Panic: attempt to subtract with overflow" Autoharness: Checking function Duration::abs_diff against all possible inputs... Duration::checked_sub\ - Status: SUCCESS\ - - Description: "attempt to subtract with overflow" + - Description: "Panic: attempt to subtract with overflow" Duration::checked_sub\ - Status: SUCCESS\ - - Description: "attempt to subtract with overflow" + - Description: "Panic: attempt to subtract with overflow" Autoharness: Checking function Duration::new's contract against all possible inputs... Nanoseconds::new_unchecked\ - Status: SUCCESS\ - - Description: "val < NANOS_PER_SEC" + - Description: "Panic: val < NANOS_PER_SEC" Duration::new\ - Status: SUCCESS\ - - Description: "|duration| duration.is_safe()" + - Description: "Panic: |duration| duration.is_safe()" std::option::expect_failed\ - Status: FAILURE\ - - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Description: "Panic: This is a placeholder message; Kani doesn't support message formatted at runtime" Autoharness Summary: diff --git a/tests/script-based-pre/playback_array/playback_array.expected b/tests/script-based-pre/playback_array/playback_array.expected index ef1ffa7f2f93..06031a9ef0ce 100644 --- a/tests/script-based-pre/playback_array/playback_array.expected +++ b/tests/script-based-pre/playback_array/playback_array.expected @@ -1,4 +1,4 @@ -Failed Checks: index out of bounds: the length is less than or equal to the given index +Failed Checks: Panic: index out of bounds: the length is less than or equal to the given index VERIFICATION:- FAILED @@ -6,4 +6,4 @@ INFO: Now modifying the source code to include the concrete playback unit test: running 1 test -index out of bounds: the len is 65 but the index is \ No newline at end of file +index out of bounds: the len is 65 but the index is diff --git a/tests/ui/cbmc_checks/pointer/expected b/tests/ui/cbmc_checks/pointer/expected index 5a1d87cf2e3d..b2a6ed3aacdd 100644 --- a/tests/ui/cbmc_checks/pointer/expected +++ b/tests/ui/cbmc_checks/pointer/expected @@ -1,2 +1,2 @@ Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment -Failed Checks: assertion failed: unsafe { *p1 != 0 } +Failed Checks: Panic: assertion failed: unsafe { *p1 != 0 } diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 80d3eef3cd25..e537bd6e04e9 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -1,9 +1,9 @@ -Failed Checks: attempt to add with overflow -Failed Checks: attempt to subtract with overflow -Failed Checks: attempt to multiply with overflow -Failed Checks: attempt to divide by zero -Failed Checks: attempt to divide with overflow -Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: attempt to calculate the remainder with overflow -Failed Checks: attempt to shift left with overflow -Failed Checks: attempt to shift right with overflow +Failed Checks: Panic: attempt to add with overflow +Failed Checks: Panic: attempt to subtract with overflow +Failed Checks: Panic: attempt to multiply with overflow +Failed Checks: Panic: attempt to divide by zero +Failed Checks: Panic: attempt to divide with overflow +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero +Failed Checks: Panic: attempt to calculate the remainder with overflow +Failed Checks: Panic: attempt to shift left with overflow +Failed Checks: Panic: attempt to shift right with overflow diff --git a/tests/ui/cbmc_checks/unsigned-overflow/expected b/tests/ui/cbmc_checks/unsigned-overflow/expected index fd6e760da3c8..c6140c359237 100644 --- a/tests/ui/cbmc_checks/unsigned-overflow/expected +++ b/tests/ui/cbmc_checks/unsigned-overflow/expected @@ -1,7 +1,7 @@ -Failed Checks: attempt to divide by zero -Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: attempt to add with overflow -Failed Checks: attempt to subtract with overflow -Failed Checks: attempt to multiply with overflow -Failed Checks: attempt to shift right with overflow -Failed Checks: attempt to shift left with overflow +Failed Checks: Panic: attempt to divide by zero +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero +Failed Checks: Panic: attempt to add with overflow +Failed Checks: Panic: attempt to subtract with overflow +Failed Checks: Panic: attempt to multiply with overflow +Failed Checks: Panic: attempt to shift right with overflow +Failed Checks: Panic: attempt to shift left with overflow diff --git a/tests/ui/check_operations/expected b/tests/ui/check_operations/expected index 4ae71e2a88a6..52d12bfa51c8 100644 --- a/tests/ui/check_operations/expected +++ b/tests/ui/check_operations/expected @@ -1,9 +1,9 @@ -Failed Checks: attempt to add with overflow -Failed Checks: attempt to subtract with overflow -Failed Checks: attempt to multiply with overflow -Failed Checks: attempt to divide by zero -Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: attempt to shift left with overflow -Failed Checks: attempt to shift right with overflow -Failed Checks: attempt to negate with overflow -Failed Checks: index out of bounds: the length is less than or equal to the given index +Failed Checks: Panic: attempt to add with overflow +Failed Checks: Panic: attempt to subtract with overflow +Failed Checks: Panic: attempt to multiply with overflow +Failed Checks: Panic: attempt to divide by zero +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero +Failed Checks: Panic: attempt to shift left with overflow +Failed Checks: Panic: attempt to shift right with overflow +Failed Checks: Panic: attempt to negate with overflow +Failed Checks: Panic: index out of bounds: the length is less than or equal to the given index diff --git a/tests/ui/derive-arbitrary/enum/expected b/tests/ui/derive-arbitrary/enum/expected index 3cfdb62d878d..4ce484d55701 100644 --- a/tests/ui/derive-arbitrary/enum/expected +++ b/tests/ui/derive-arbitrary/enum/expected @@ -1,15 +1,15 @@ Checking harness check_comparison... SUCCESS\ -"assertion failed: disc >= -1 && disc <= 1" +"Panic: assertion failed: disc >= -1 && disc <= 1" SUCCESS\ -"assertion failed: disc == 1" +"Panic: assertion failed: disc == 1" SUCCESS\ -"assertion failed: disc == -1" +"Panic: assertion failed: disc == -1" SUCCESS\ -"assertion failed: disc == 0" +"Panic: assertion failed: disc == 0" Checking harness check_enum_wrapper... diff --git a/tests/ui/derive-arbitrary/single_variant_enum/expected b/tests/ui/derive-arbitrary/single_variant_enum/expected index 35ea4d3a01ba..522399c1b5d8 100644 --- a/tests/ui/derive-arbitrary/single_variant_enum/expected +++ b/tests/ui/derive-arbitrary/single_variant_enum/expected @@ -1,15 +1,15 @@ Checking harness check_with_discriminant... SUCCESS\ -"assertion failed: disc == 42" +"Panic: assertion failed: disc == 42" Checking harness check_with_named_args... SUCCESS\ -"assertion failed: flag as u8 == 0 || flag as u8 == 1" +"Panic: assertion failed: flag as u8 == 0 || flag as u8 == 1" 2 of 2 cover properties satisfied Checking harness check_with_args... SUCCESS\ -"assertion failed: c <= char::MAX" +"Panic: assertion failed: c <= char::MAX" 2 of 2 cover properties satisfied Checking harness check_simple... diff --git a/tests/ui/duplicates/expected b/tests/ui/duplicates/expected index 9e6b135283d6..526cfb807561 100644 --- a/tests/ui/duplicates/expected +++ b/tests/ui/duplicates/expected @@ -3,11 +3,11 @@ Checking harness check_remainder... RESULTS: check_remainder.assertion\ Status: FAILURE\ -Description: "attempt to calculate the remainder with a divisor of zero" +Description: "Panic: attempt to calculate the remainder with a divisor of zero" check_remainder.assertion\ Status: FAILURE\ -Description: "attempt to calculate the remainder with overflow" +Description: "Panic: attempt to calculate the remainder with overflow" check_remainder.arithmetic_overflow\ Status: SUCCESS\ @@ -21,17 +21,17 @@ check_remainder.division-by-zero\ Status: SUCCESS\ Description: "division by zero" -Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: attempt to calculate the remainder with overflow +Failed Checks: Panic: attempt to calculate the remainder with a divisor of zero +Failed Checks: Panic: attempt to calculate the remainder with overflow Checking harness check_division... check_division.assertion\ Status: FAILURE\ -Description: "attempt to divide by zero" +Description: "Panic: attempt to divide by zero" check_division.assertion\ Status: FAILURE\ -Description: "attempt to divide with overflow" +Description: "Panic: attempt to divide with overflow" check_division.arithmetic_overflow\ Status: SUCCESS\ @@ -45,5 +45,5 @@ check_division.division-by-zero\ Status: SUCCESS\ Description: "division by zero" -Failed Checks: attempt to divide by zero -Failed Checks: attempt to divide with overflow +Failed Checks: Panic: attempt to divide by zero +Failed Checks: Panic: attempt to divide with overflow diff --git a/tests/ui/extern_std/macro_override.expected b/tests/ui/extern_std/macro_override.expected index feacbd7b5be6..3a44a4027b7a 100644 --- a/tests/ui/extern_std/macro_override.expected +++ b/tests/ui/extern_std/macro_override.expected @@ -1,7 +1,7 @@ Checking harness foo... Status: SUCCESS\ -Description: ""debug_assert""\ +Description: "Panic: "debug_assert""\ macro_override.rs: Status: SUCCESS\ diff --git a/tests/ui/missing-function/extern_c/expected b/tests/ui/missing-function/extern_c/expected index eab619abc0d9..c6c6daa4a79c 100644 --- a/tests/ui/missing-function/extern_c/expected +++ b/tests/ui/missing-function/extern_c/expected @@ -1,5 +1,5 @@ Status: UNDETERMINED\ -Description: "assertion failed: x == 5" +Description: "Panic: assertion failed: x == 5" Status: FAILURE\ Description: "Function `missing_function` with missing definition is unreachable" VERIFICATION:- FAILED diff --git a/tests/ui/regular-output-format-fail/expected b/tests/ui/regular-output-format-fail/expected index 25fe5daa3089..1021d68e4537 100644 --- a/tests/ui/regular-output-format-fail/expected +++ b/tests/ui/regular-output-format-fail/expected @@ -1,2 +1,2 @@ -Description: "assertion failed: 1 + 1 == 3" -Failed Checks: assertion failed: 1 + 1 == 3 +Description: "Panic: assertion failed: 1 + 1 == 3" +Failed Checks: Panic: assertion failed: 1 + 1 == 3 diff --git a/tests/ui/regular-output-format-pass/expected b/tests/ui/regular-output-format-pass/expected index d72e119a90d1..8ee8f7117f38 100644 --- a/tests/ui/regular-output-format-pass/expected +++ b/tests/ui/regular-output-format-pass/expected @@ -1,3 +1,3 @@ -Description: "assertion failed: 1 + 1 == 2"\ +Description: "Panic: assertion failed: 1 + 1 == 2"\ Location: tests/ui/regular-output-format-pass/main.rs:7:5 in function main diff --git a/tests/ui/terse-output-format-fail/expected b/tests/ui/terse-output-format-fail/expected index 9d88112f2998..45c1bcb0b1e2 100644 --- a/tests/ui/terse-output-format-fail/expected +++ b/tests/ui/terse-output-format-fail/expected @@ -1,2 +1,2 @@ VERIFICATION RESULT: -Failed Checks: assertion failed: 1 + 1 == 3 +Failed Checks: Panic: assertion failed: 1 + 1 == 3