Skip to content

Commit f49d76b

Browse files
committed
Upgrade toolchain to nightly-2025-01-17
Changes required due to - rust-lang/rust#135344: Less unsafe in `dangling`/`without_provenance` Resolves: model-checking#3840
1 parent 6f70c7d commit f49d76b

File tree

3 files changed

+6
-4
lines changed

3 files changed

+6
-4
lines changed

rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-01-16"
5+
channel = "nightly-2025-01-17"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
Checking harness pre_condition::harness_invalid_ptr...
2-
VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
2+
Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20
3+
Failed Checks: Kani does not support reasoning about pointer to unallocated memory
4+
Failed Checks: dereference failure: pointer outside object bounds
5+
VERIFICATION:- FAILED
36

47
Checking harness pre_condition::harness_stack_ptr...
58
VERIFICATION:- SUCCESSFUL
69

710
Checking harness pre_condition::harness_head_ptr...
811
VERIFICATION:- SUCCESSFUL
912

10-
Complete - 3 successfully verified harnesses, 0 failures, 3 total
13+
Complete - 2 successfully verified harnesses, 1 failures, 3 total

tests/expected/function-contract/valid_ptr.rs

-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ mod pre_condition {
2828
}
2929

3030
#[kani::proof_for_contract(read_ptr)]
31-
#[kani::should_panic]
3231
fn harness_invalid_ptr() {
3332
let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
3433
assert_eq!(unsafe { read_ptr(ptr) }, -20);

0 commit comments

Comments
 (0)