From 8a03176a696f9dc3f475a10df7c76633efb3c817 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 09:54:11 +0200
Subject: [PATCH] [tests] add test for generalized check

---
 tests/spec/generalized_check.i                | 16 ++++++++++++
 .../spec/oracle/generalized_check.res.oracle  | 25 +++++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 tests/spec/generalized_check.i
 create mode 100644 tests/spec/oracle/generalized_check.res.oracle

diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
new file mode 100644
index 00000000000..1409e3efc7a
--- /dev/null
+++ b/tests/spec/generalized_check.i
@@ -0,0 +1,16 @@
+/*@ check lemma tauto: \true ==> \true; */
+
+/*@ check requires \valid(x);
+    assigns *x;
+    check ensures *x == 0;
+*/
+void f(int* x) {
+  /*@ check \valid(x); */ // can't be proved by WP: we ignore the requires
+  *x = 0;
+}
+
+int main() {
+  int a = 4;
+  f(&a);
+  /*@ check a == 0; */ // can't be proved by WP: we ignore the ensures
+}
diff --git a/tests/spec/oracle/generalized_check.res.oracle b/tests/spec/oracle/generalized_check.res.oracle
new file mode 100644
index 00000000000..7017e6e7b84
--- /dev/null
+++ b/tests/spec/oracle/generalized_check.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ check lemma tauto: \true;
+ */
+/*@ check requires \valid(x);
+    check ensures *\old(x) ≡ 0;
+    assigns *x; */
+void f(int *x)
+{
+  /*@ check \valid(x); */ ;
+  *x = 0;
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int a = 4;
+  f(& a);
+  /*@ check a ≡ 0; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+
-- 
GitLab