Add a test

creusot-rs · Nov 27, 2024 · 05b4792 · 05b4792
1 parent 81d5434
commit 05b4792
Show file tree

Hide file tree

Showing 4 changed files with 156 additions and 0 deletions.
diff --git a/creusot/tests/should_succeed/fmap_indexing.coma b/creusot/tests/should_succeed/fmap_indexing.coma
diff --git a/creusot/tests/should_succeed/fmap_indexing.rs b/creusot/tests/should_succeed/fmap_indexing.rs
@@ -0,0 +1,12 @@
+extern crate creusot_contracts;
+use creusot_contracts::{logic::FMap, *};
+
+pub fn foo() {
+    let mut map = snapshot!(FMap::empty());
+    map = snapshot!(map.insert(1, 3));
+    proof_assert!(map[1] == 3);
+    map = snapshot!(map.insert(2, 42));
+    proof_assert!(map[1] == 3 && map[2] == 42);
+    map = snapshot!(map.insert(1, 4));
+    proof_assert!(map[1] == 4 && map[2] == 42);
+}
diff --git a/creusot/tests/should_succeed/fmap_indexing/why3session.xml b/creusot/tests/should_succeed/fmap_indexing/why3session.xml
diff --git a/creusot/tests/should_succeed/fmap_indexing/why3shapes.gz b/creusot/tests/should_succeed/fmap_indexing/why3shapes.gz