Add a test

creusot-rs · Dec 10, 2024 · e2144a8 · e2144a8
1 parent c66f258
commit e2144a8
Show file tree

Hide file tree

Showing 4 changed files with 99 additions and 0 deletions.
diff --git a/creusot/tests/should_succeed/mapping_indexing.coma b/creusot/tests/should_succeed/mapping_indexing.coma
diff --git a/creusot/tests/should_succeed/mapping_indexing.rs b/creusot/tests/should_succeed/mapping_indexing.rs
@@ -0,0 +1,15 @@
+extern crate creusot_contracts;
+use creusot_contracts::{logic::Mapping, *};
+
+pub fn foo() {
+    let mut mapping = snapshot!(Mapping::unknown());
+
+    mapping = snapshot!(mapping.set(0, 2));
+    proof_assert!(mapping[0] == 2);
+    mapping = snapshot!(mapping.set(1, 3));
+    proof_assert!(mapping[0] == 2);
+    proof_assert!(mapping[1] == 3);
+    mapping = snapshot!(mapping.set(0, 4));
+    proof_assert!(mapping[1] == 3);
+    proof_assert!(mapping[0] == 4);
+}
diff --git a/creusot/tests/should_succeed/mapping_indexing/why3session.xml b/creusot/tests/should_succeed/mapping_indexing/why3session.xml
diff --git a/creusot/tests/should_succeed/mapping_indexing/why3shapes.gz b/creusot/tests/should_succeed/mapping_indexing/why3shapes.gz