Add a test

creusot-rs · Nov 28, 2024 · 21f5931 · 21f5931
1 parent d14b7d8
commit 21f5931
Show file tree

Hide file tree

Showing 5 changed files with 121 additions and 5 deletions.
diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
diff --git a/creusot/tests/should_succeed/ghost/snapshot_in_ghost.coma b/creusot/tests/should_succeed/ghost/snapshot_in_ghost.coma
diff --git a/creusot/tests/should_succeed/ghost/snapshot_in_ghost.rs b/creusot/tests/should_succeed/ghost/snapshot_in_ghost.rs
@@ -0,0 +1,17 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+// Check that we can make snapshots in ghost code.
+pub fn foo() {
+    ghost! {
+        let x = snapshot!(1);
+        proof_assert!(*x == 1);
+    };
+}
+
+// Check that we can make snapshots in pure functions.
+#[pure]
+pub fn is_pure() {
+    let x = snapshot!(1);
+    proof_assert!(*x == 1);
+}
diff --git a/creusot/tests/should_succeed/ghost/snapshot_in_ghost/why3session.xml b/creusot/tests/should_succeed/ghost/snapshot_in_ghost/why3session.xml
diff --git a/creusot/tests/should_succeed/ghost/snapshot_in_ghost/why3shapes.gz b/creusot/tests/should_succeed/ghost/snapshot_in_ghost/why3shapes.gz