From cac90c5f843f95cf448754a54d5d6b20d2a039ee Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Fri, 22 Mar 2024 12:15:44 -0700
Subject: [PATCH] Update harness name and expand the test description

---
 tests/kani/Spurious/storage_fixme.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/kani/Spurious/storage_fixme.rs b/tests/kani/Spurious/storage_fixme.rs
index f67b8e6fa742..51d13f31bcef 100644
--- a/tests/kani/Spurious/storage_fixme.rs
+++ b/tests/kani/Spurious/storage_fixme.rs
@@ -5,6 +5,9 @@
 
 // Our handling of storage markers causes spurious failures in this test.
 // https://github.com/model-checking/kani/issues/3099
+// The code is extracted from the implementation of `BTreeMap` which is where we
+// originally saw the spurious failures while trying to enable storage markers
+// for `std` in https://github.com/model-checking/kani/pull/3080
 
 use std::alloc::Layout;
 use std::marker::PhantomData;
@@ -640,7 +643,7 @@ struct IntoIter {
 }
 
 #[cfg_attr(kani, kani::proof, kani::unwind(3))]
-fn main() {
+fn check_storagemarker_btreemap() {
     let mut f = Foo { root: None, length: 0 };
     let mut root: NodeRef<marker::Owned, marker::Leaf> = NodeRef::new_leaf();
     root.borrow_mut().push();