Merge remote-tracking branch 'origin/main' into enable-post_condition

tautschnig · Jan 22, 2025 · fd126f6 · fd126f6
2 parents f5f369b + f8a1488
commit fd126f6
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 16 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
@@ -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/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -84,16 +84,13 @@ where
         .iter()
         .filter_map(|item| {
             // Only collect monomorphic items.
-            // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released.
-            let def_id = rustc_internal::internal(tcx, item.def_id());
-            (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..))
-                || matches!(item.kind(), ItemKind::Fn))
-            .then(|| {
-                Instance::try_from(*item)
-                    .ok()
-                    .and_then(|instance| predicate(tcx, instance).then_some(instance))
-            })
-            .flatten()
+            matches!(item.kind(), ItemKind::Fn)
+                .then(|| {
+                    Instance::try_from(*item)
+                        .ok()
+                        .and_then(|instance| predicate(tcx, instance).then_some(instance))
+                })
+                .flatten()
         })
         .collect::<Vec<_>>()
 }

diff --git 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
@@ -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
@@ -4,12 +4,15 @@ Failed Checks: |result| kani::mem::can_dereference(result.0)
 VERIFICATION:- FAILED
 
 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
 
 Checking harness pre_condition::harness_head_ptr...
 VERIFICATION:- SUCCESSFUL
 
-Complete - 3 successfully verified harnesses, 1 failures, 4 total
+Complete - 2 successfully verified harnesses, 2 failures, 4 total
diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs
@@ -26,7 +26,6 @@ mod pre_condition {
     }
 
     #[kani::proof_for_contract(read_ptr)]
-    #[kani::should_panic]
     fn harness_invalid_ptr() {
         let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
         assert_eq!(unsafe { read_ptr(ptr) }, -20);