Skip to content

Commit cac90c5

Browse files
committed
Update harness name and expand the test description
1 parent b05e60e commit cac90c5

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

tests/kani/Spurious/storage_fixme.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55

66
// Our handling of storage markers causes spurious failures in this test.
77
// https://github.com/model-checking/kani/issues/3099
8+
// The code is extracted from the implementation of `BTreeMap` which is where we
9+
// originally saw the spurious failures while trying to enable storage markers
10+
// for `std` in https://github.com/model-checking/kani/pull/3080
811

912
use std::alloc::Layout;
1013
use std::marker::PhantomData;
@@ -640,7 +643,7 @@ struct IntoIter {
640643
}
641644

642645
#[cfg_attr(kani, kani::proof, kani::unwind(3))]
643-
fn main() {
646+
fn check_storagemarker_btreemap() {
644647
let mut f = Foo { root: None, length: 0 };
645648
let mut root: NodeRef<marker::Owned, marker::Leaf> = NodeRef::new_leaf();
646649
root.borrow_mut().push();

0 commit comments

Comments
 (0)