From 511953da585a1517125a936ace70b33205041f69 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jan 2025 14:09:45 +0100 Subject: [PATCH] Upgrade toolchain to nightly-2025-01-22 (#3843) Changes required due to - rust-lang/rust#135344: Less unsafe in `dangling`/`without_provenance` - rust-lang/rust#135661: Stabilize `float_next_up_down` - rust-lang/rust#135709: Temporarily bring back `Rvalue::Len` Resolves: #3840 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/kani_middle/points_to/points_to_analysis.rs | 2 +- kani-compiler/src/main.rs | 1 - rust-toolchain.toml | 2 +- tests/expected/function-contract/valid_ptr.expected | 7 +++++-- tests/expected/function-contract/valid_ptr.rs | 1 - 5 files changed, 7 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 834b3e4026c4..3d80397530b3 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -575,7 +575,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // The same story from BinOp applies here, too. Need to track those things. self.successors_for_operand(state, operand) } - Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => { + Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) | Rvalue::Len(_) => { // All of those should yield a constant. HashSet::new() } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 02709797cf3a..65424f6d46bf 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -16,7 +16,6 @@ #![feature(f128)] #![feature(f16)] #![feature(non_exhaustive_omitted_patterns_lint)] -#![feature(float_next_up_down)] #![feature(try_blocks)] extern crate rustc_abi; extern crate rustc_ast; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 65c4ff69756c..114ca7ffa2aa 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-01-16" +channel = "nightly-2025-01-22" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 4014a0723029..0f8100c7ceeb 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,8 @@ Checking harness pre_condition::harness_invalid_ptr... -VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +Failed Checks: 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 Checking harness pre_condition::harness_stack_ptr... VERIFICATION:- SUCCESSFUL @@ -7,4 +10,4 @@ VERIFICATION:- SUCCESSFUL Checking harness pre_condition::harness_head_ptr... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total +Complete - 2 successfully verified harnesses, 1 failures, 3 total diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs index 2047a46caf4f..9537ecc30daa 100644 --- a/tests/expected/function-contract/valid_ptr.rs +++ b/tests/expected/function-contract/valid_ptr.rs @@ -28,7 +28,6 @@ mod pre_condition { } #[kani::proof_for_contract(read_ptr)] - #[kani::should_panic] fn harness_invalid_ptr() { let ptr = std::ptr::NonNull::::dangling().as_ptr(); assert_eq!(unsafe { read_ptr(ptr) }, -20);