fix tests

model-checking · Jul 17, 2024 · 0bbd78b · 0bbd78b
1 parent ed8fee1
commit 0bbd78b
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 4 deletions.
diff --git a/tests/expected/function-contract/interior-mutability/cell.expected b/tests/expected/function-contract/interior-mutability/cell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{x.x.hack()}.value.value < 101"\
-in function max
+- Description: "|_| unsafe{ x.x.hack() }.value.value < 101"\
+in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/cell.rs b/tests/expected/function-contract/interior-mutability/cell.rs
@@ -1,3 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
 use std::cell::{Cell, RefCell, UnsafeCell};
 use std::mem::transmute;
 use std::panic;

diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.expected b/tests/expected/function-contract/interior-mutability/unsafecell.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{x.x.hack()}.value < 101"\
-in function max
+- Description: "|_| unsafe{ x.x.hack() }.value < 101"\
+in function modify
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/unsafecell.rs b/tests/expected/function-contract/interior-mutability/unsafecell.rs
@@ -1,3 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
 use std::cell::{Cell, RefCell, UnsafeCell};
 use std::mem::transmute;
 use std::panic;