move test

model-checking · Oct 23, 2024 · 0c82f57 · 0c82f57
1 parent 28d1288
commit 0c82f57
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/tests/expected/issue-3631/issue-3631.expected b/tests/expected/issue-3631/issue-3631.expected
diff --git a/tests/expected/issue-3631/issue-3631.rs → ...CodegenAggregateRawPtrTraitObject/main.rs b/tests/expected/issue-3631/issue-3631.rs → ...CodegenAggregateRawPtrTraitObject/main.rs
@@ -1,5 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// Test that Kani can verify code that produces a aggregate raw pointer to trait objects
+// c.f. https://github.com/model-checking/kani/issues/3631
 
 #![feature(ptr_metadata)]
 
@@ -21,7 +23,7 @@ impl SampleTrait for SampleStruct {
 
 #[cfg(kani)]
 #[kani::proof]
-fn main() {
+fn check_nonnull_dyn_from_raw_parts() {
     // Create a SampleTrait object from SampleStruct
     let sample_struct = SampleStruct { value: kani::any() };
     let trait_object: &dyn SampleTrait = &sample_struct;