diff --git a/tests/expected/loop-backedge/see b/tests/expected/loop-backedge/see deleted file mode 100644 index 44cfecdc308e..000000000000 --- a/tests/expected/loop-backedge/see +++ /dev/null @@ -1,654 +0,0 @@ -Checking harness check_unwind_assertion... -CBMC 5.72.0 (cbmc-5.72.0) -CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux -Reading GOTO program from file test.for-check_unwind_assertion.out -Generating GOTO Program -Adding CPROVER library (x86_64) -Removal of function pointers and virtual functions -Generic Property Instrumentation -Running with 16 object bits, 48 offset bits (user-specified) -Starting Bounded Model Checking -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -Unwinding loop test::check_unwind_assertion.1 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Unwinding loop test::check_unwind_assertion.0 iteration 1 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -Unwinding loop test::check_unwind_assertion.1 iteration 2 file /home/ubuntu/git/kani/tests/expected/loop-backedge/test.rs line 14 column 13 function check_unwind_assertion thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs line 38 column 15 function std::ptr::mut_ptr::::is_null thread 0 -aborting path on assume(false) at file /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs line 39 column 15 function std::ptr::const_ptr::::is_null thread 0 -Runtime Symex: 0.074707s -size of program expression: 2737 steps -slicing removed 1810 assignments -Generated 350 VCC(s), 76 remaining after simplification -Runtime Postprocess Equation: 0.000470442s -Passing problem to propositional reduction -converting SSA -Runtime Convert SSA: 0.00704614s -Running propositional reduction -Post-processing -Runtime Post-process: 5.37e-06s -Solving with MiniSAT 2.2.1 with simplifier -7849 variables, 11571 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00362767s -Runtime decision procedure: 0.010891s -Running propositional reduction -Solving with MiniSAT 2.2.1 with simplifier -7849 variables, 274 clauses -SAT checker: instance is UNSATISFIABLE -Runtime Solver: 0.00043837s -Runtime decision procedure: 0.000479132s - -RESULTS: -Check 1: std::ptr::write::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 2: std::ptr::write::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 3: std::ptr::write::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 4: std::ptr::const_ptr::::is_null.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null - -Check 5: std::ptr::mut_ptr::::is_null.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null - -Check 6: check_unwind_assertion.assertion.1 - - Status: SUCCESS - - Description: "assertion failed: e == 0" - - Location: test.rs:12:9 in function check_unwind_assertion - -Check 7: check_unwind_assertion.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: test.rs:11:15 in function check_unwind_assertion - -Check 8: check_unwind_assertion.assertion.2 - - Status: SUCCESS - - Description: "assertion failed: i == 0" - - Location: test.rs:14:13 in function check_unwind_assertion - -Check 9: check_unwind_assertion.unreachable.2 - - Status: SUCCESS - - Description: "unreachable code" - - Location: test.rs:13:18 in function check_unwind_assertion - -Check 10: core::num::::unchecked_add.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to compute unchecked_add which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/int_macros.rs:460:22 in function core::num::::unchecked_add - -Check 11: std::ptr::const_ptr::::offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset - -Check 12: std::ptr::const_ptr::::offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:456:18 in function std::ptr::const_ptr::::offset - -Check 13: std::slice::Iter::<'_, i32>::new.assume.1 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:92:13 in function std::slice::Iter::<'_, i32>::new - -Check 14: std::ptr::mut_ptr::::offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset - -Check 15: std::ptr::mut_ptr::::offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:470:18 in function std::ptr::mut_ptr::::offset - -Check 16: as std::iter::Iterator>::next.assume.1 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:21 in function as std::iter::Iterator>::next - -Check 17: as std::iter::Iterator>::next.assume.2 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:25 in function as std::iter::Iterator>::next - -Check 18: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "arith_offset: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset - -Check 19: std::ptr::const_ptr::::wrapping_offset.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:538:18 in function std::ptr::const_ptr::::wrapping_offset - -Check 20: std::ptr::read::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 21: std::ptr::read::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 22: std::ptr::read::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 23: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 24: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 25: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 26: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 27: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 28: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:29 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 29: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 30: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 31: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 32: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 33: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 34: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:67:17 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 35: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 36: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 37: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 38: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 39: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 40: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:88:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 41: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 42: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 43: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 44: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 45: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 46: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:90:31 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 47: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 48: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.26 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 49: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.27 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 50: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.28 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 51: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.29 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 52: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.30 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:64 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 53: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.31 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 54: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.32 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 55: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.33 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 56: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.34 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 57: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.35 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 58: std::slice::Iter::<'_, i32>::post_inc_start.pointer_dereference.36 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:93:21 in function std::slice::Iter::<'_, i32>::post_inc_start - -Check 59: memcpy.pointer.1 - - Status: SUCCESS - - Description: "same object violation" - - Location: :33 in function memcpy - -Check 60: memcpy.pointer.2 - - Status: SUCCESS - - Description: "same object violation" - - Location: :34 in function memcpy - -Check 61: std::ptr::read::.precondition_instance.1 - - Status: SUCCESS - - Description: "memcpy src/dst overlap" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 62: std::ptr::read::.precondition_instance.2 - - Status: SUCCESS - - Description: "memcpy source region readable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 63: std::ptr::read::.precondition_instance.3 - - Status: SUCCESS - - Description: "memcpy destination region writeable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1133:9 in function std::ptr::read:: - -Check 64: memcpy.pointer.3 - - Status: SUCCESS - - Description: "same object violation" - - Location: :33 in function memcpy - -Check 65: memcpy.pointer.4 - - Status: SUCCESS - - Description: "same object violation" - - Location: :34 in function memcpy - -Check 66: std::ptr::write::.precondition_instance.1 - - Status: SUCCESS - - Description: "memcpy src/dst overlap" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 67: std::ptr::write::.precondition_instance.2 - - Status: SUCCESS - - Description: "memcpy source region readable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 68: std::ptr::write::.precondition_instance.3 - - Status: SUCCESS - - Description: "memcpy destination region writeable" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1330:9 in function std::ptr::write:: - -Check 69: std::ptr::const_ptr::::is_null.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:39:15 in function std::ptr::const_ptr::::is_null - -Check 70: std::ptr::const_ptr::::guaranteed_eq.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:819:18 in function std::ptr::const_ptr::::guaranteed_eq - -Check 71: std::cmp::impls::::lt.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 72: std::cmp::impls::::lt.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 73: std::cmp::impls::::lt.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 74: std::cmp::impls::::lt.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 75: std::cmp::impls::::lt.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 76: std::cmp::impls::::lt.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:52 in function std::cmp::impls::::lt - -Check 77: std::cmp::impls::::lt.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 78: std::cmp::impls::::lt.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 79: std::cmp::impls::::lt.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 80: std::cmp::impls::::lt.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 81: std::cmp::impls::::lt.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 82: std::cmp::impls::::lt.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs:1464:62 in function std::cmp::impls::::lt - -Check 83: as std::iter::Iterator>::next.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 84: as std::iter::Iterator>::next.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 85: as std::iter::Iterator>::next.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 86: as std::iter::Iterator>::next.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 87: as std::iter::Iterator>::next.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 88: as std::iter::Iterator>::next.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:142:29 in function as std::iter::Iterator>::next - -Check 89: as std::iter::Iterator>::next.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 90: as std::iter::Iterator>::next.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 91: as std::iter::Iterator>::next.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 92: as std::iter::Iterator>::next.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 93: as std::iter::Iterator>::next.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 94: as std::iter::Iterator>::next.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:144:33 in function as std::iter::Iterator>::next - -Check 95: as std::iter::Iterator>::next.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 96: as std::iter::Iterator>::next.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 97: as std::iter::Iterator>::next.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 98: as std::iter::Iterator>::next.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 99: as std::iter::Iterator>::next.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 100: as std::iter::Iterator>::next.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:9 in function as std::iter::Iterator>::next - -Check 101: as std::iter::Iterator>::next.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 102: as std::iter::Iterator>::next.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 103: as std::iter::Iterator>::next.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 104: as std::iter::Iterator>::next.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 105: as std::iter::Iterator>::next.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 106: as std::iter::Iterator>::next.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:8:43 in function as std::iter::Iterator>::next - -Check 107: as std::iter::Iterator>::next.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:147:25 in function as std::iter::Iterator>::next - -Check 108: check_unwind_assertion.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: test.rs:11:15 in function check_unwind_assertion - -Check 109: check_unwind_assertion.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 110: check_unwind_assertion.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 111: check_unwind_assertion.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 112: check_unwind_assertion.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 113: check_unwind_assertion.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 114: check_unwind_assertion.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: test.rs:11:10 in function check_unwind_assertion - -Check 115: std::clone::impls::::clone.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 116: std::clone::impls::::clone.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 117: std::clone::impls::::clone.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 118: std::clone::impls::::clone.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 119: std::clone::impls::::clone.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 120: std::clone::impls::::clone.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/clone.rs:190:25 in function std::clone::impls::::clone - -Check 121: std::ptr::mut_ptr::::is_null.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs:38:15 in function std::ptr::mut_ptr::::is_null - - -SUMMARY: - ** 0 of 121 failed - -VERIFICATION:- SUCCESSFUL -Verification Time: 0.178895s - diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml new file mode 100644 index 000000000000..41fa0a2db3ba --- /dev/null +++ b/tests/perf/btreeset/insert_any/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "insert_any" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/perf/btreeset/insert_any/expected b/tests/perf/btreeset/insert_any/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/btreeset/insert_any/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/btreeset/insert_any/src/main.rs b/tests/perf/btreeset/insert_any/src/main.rs new file mode 100644 index 000000000000..198970037b36 --- /dev/null +++ b/tests/perf/btreeset/insert_any/src/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of pushing onto a BTreeSet +//! The test is from https://github.com/model-checking/kani/issues/705. +//! Pre CBMC 5.72.0, it ran out of memory +//! With CBMC 5.72.0, it takes ~10 seconds and consumes ~255 MB of memory. + +use std::collections::BTreeSet; + +#[kani::proof] +#[kani::unwind(3)] +fn main() { + let mut set = BTreeSet::::new(); + set.insert(kani::any()); +}