Add a test for PtrOwn disjointness

creusot-rs · Dec 9, 2024 · 26f39be · 26f39be
1 parent e5afa1f
commit 26f39be
Show file tree

Hide file tree

Showing 4 changed files with 344 additions and 0 deletions.
diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.coma b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.coma
diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs
@@ -0,0 +1,13 @@
+extern crate creusot_contracts;
+use creusot_contracts::{ptr_own::PtrOwn, *};
+
+pub fn foo() {
+    let (p1, mut own1) = PtrOwn::new(1i32);
+    let (p2, own2) = PtrOwn::new(1i32);
+
+    ghost! {
+        let _ = PtrOwn::disjoint_lemma(*own1.borrow_mut(), *own2.borrow());
+    };
+    proof_assert!(own1 != own2);
+    proof_assert!(p1 != p2);
+}
diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3session.xml b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3session.xml
diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3shapes.gz b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3shapes.gz