Add a test

creusot-rs · Nov 28, 2024 · 118c7eb · 118c7eb
1 parent e876fe6
commit 118c7eb
Show file tree

Hide file tree

Showing 4 changed files with 107 additions and 0 deletions.
diff --git a/creusot/tests/should_succeed/syntax/int_suffix.coma b/creusot/tests/should_succeed/syntax/int_suffix.coma
diff --git a/creusot/tests/should_succeed/syntax/int_suffix.rs b/creusot/tests/should_succeed/syntax/int_suffix.rs
@@ -0,0 +1,7 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+#[ensures(*result == 1int)]
+pub fn foo() -> GhostBox<Int> {
+    ghost!(1int)
+}
diff --git a/creusot/tests/should_succeed/syntax/int_suffix/why3session.xml b/creusot/tests/should_succeed/syntax/int_suffix/why3session.xml
diff --git a/creusot/tests/should_succeed/syntax/int_suffix/why3shapes.gz b/creusot/tests/should_succeed/syntax/int_suffix/why3shapes.gz