From 8af65bee123991376ef6f74a41f5a709231218d2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 29 Aug 2024 15:54:15 +0200
Subject: [PATCH] [tests] prepare test for inline-stmt-contracts transformation
---
tests/syntax/inline_stmt_contract.i | 44 +++++++++++++++++++
.../oracle/inline_stmt_contract.res.oracle | 0
2 files changed, 44 insertions(+)
create mode 100644 tests/syntax/inline_stmt_contract.i
create mode 100644 tests/syntax/oracle/inline_stmt_contract.res.oracle
diff --git a/tests/syntax/inline_stmt_contract.i b/tests/syntax/inline_stmt_contract.i
new file mode 100644
index 00000000000..551a6c461a0
--- /dev/null
+++ b/tests/syntax/inline_stmt_contract.i
@@ -0,0 +1,44 @@
+/* run.config
+OPT: -inline-stmt-contracts -print
+*/
+
+int X;
+
+int f() {
+ /*@ requires X == 0;
+ ensures X == 1;
+ */
+ X++;
+ return X;
+}
+
+int g() {
+
+ /*@ behavior b:
+ assumes X >= 0;
+ requires X > -1;
+ ensures X == 0;
+ */
+ if (X >= 0) { X = 0; } else { X = -1; }
+ return X;
+}
+
+int h() {
+ /*@ ensures \false; */
+ return 1;
+}
+
+int i() {
+ /*@ behavior b0:
+ assumes X == 0;
+ ensures X == 1;
+ */
+ X++;
+
+ /*@ behavior b1:
+ assumes X == 1;
+ ensures X == 2;
+ */
+ X++;
+ return X;
+}
diff --git a/tests/syntax/oracle/inline_stmt_contract.res.oracle b/tests/syntax/oracle/inline_stmt_contract.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab