From 0c82f57ded8841737ec385d07e208081d810e31f Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 23 Oct 2024 14:03:14 -0400
Subject: [PATCH] move test

---
 tests/expected/issue-3631/issue-3631.expected                 | 1 -
 .../CodegenAggregateRawPtrTraitObject/main.rs}                | 4 +++-
 2 files changed, 3 insertions(+), 2 deletions(-)
 delete mode 100644 tests/expected/issue-3631/issue-3631.expected
 rename tests/{expected/issue-3631/issue-3631.rs => kani/CodegenAggregateRawPtrTraitObject/main.rs} (86%)

diff --git a/tests/expected/issue-3631/issue-3631.expected b/tests/expected/issue-3631/issue-3631.expected
deleted file mode 100644
index f9a64dc8af9a..000000000000
--- a/tests/expected/issue-3631/issue-3631.expected
+++ /dev/null
@@ -1 +0,0 @@
-VERIFICATION:- SUCCESS
\ No newline at end of file
diff --git a/tests/expected/issue-3631/issue-3631.rs b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs
similarity index 86%
rename from tests/expected/issue-3631/issue-3631.rs
rename to tests/kani/CodegenAggregateRawPtrTraitObject/main.rs
index 6f1d2d2c6aa0..92ffb413ae70 100644
--- a/tests/expected/issue-3631/issue-3631.rs
+++ b/tests/kani/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;