From daeabe467b23793b0d6f166d9ea517eddadbbe26 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 18 Jan 2019 15:31:05 +0100
Subject: [PATCH] [tests] update ACSL kw test and oracles

---
 tests/spec/kw.c                             |  7 +++++-
 tests/spec/oracle/behavior_names.res.oracle |  2 +-
 tests/spec/oracle/kw.res.oracle             | 27 +++++++++++++++++++++
 3 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index 7b004bdb1c4..eb7b4e0b8fb 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -9,6 +9,7 @@ assert behavior = 0;
     ensures behavior >= 0;
 */
 int main () {
+  //@ slevel 4;
   behavior++;
   return 0;
 }
@@ -31,6 +32,10 @@ model{L}(l1,ll1) ==> model(Cons(0,l1),Cons(0,ll1));
 volatile int assigns;
 
 int ensures(volatile int* a) { return *a; }
-void requires(volatile int*a, int v) { *a = v; }
+int requires(volatile int*a, int v) { *a = v; return v; }
 
 /*@ volatile assigns reads ensures writes requires; */
+
+int slevel = 1000000;
+
+//@ lemma bar: slevel >= 0;
diff --git a/tests/spec/oracle/behavior_names.res.oracle b/tests/spec/oracle/behavior_names.res.oracle
index 2bb78b303af..f24db2ef028 100644
--- a/tests/spec/oracle/behavior_names.res.oracle
+++ b/tests/spec/oracle/behavior_names.res.oracle
@@ -78,7 +78,7 @@ void j(void)
     behavior while:
       ensures while: \true;
     
-    behavior normal:
+    behavior ensures:
       ensures ensures: \true;
     
     behavior logic:
diff --git a/tests/spec/oracle/kw.res.oracle b/tests/spec/oracle/kw.res.oracle
index 916e6673c1c..b9d920cb849 100644
--- a/tests/spec/oracle/kw.res.oracle
+++ b/tests/spec/oracle/kw.res.oracle
@@ -12,6 +12,7 @@ assert behavior = 0;
 int main(void)
 {
   int __retres;
+  /*@ slevel 4; */
   behavior ++;
   __retres = 0;
   return __retres;
@@ -25,6 +26,32 @@ inductive model{L}(List<ℤ>  root, List<ℤ>  logic_list) {
   case cons{L}: ∀ List<ℤ>  l1, List<ℤ>  ll1;
                   model(l1, ll1) ⇒ model(Cons(0, l1), Cons(0, ll1));
   }
+ */
+/*@ axiomatic foo {
+      logic ℤ func{L}(ℤ i) 
+        reads behavior;
+      
+      }
+
+*/
+int volatile assigns;
+int ensures(int volatile *a)
+{
+  int __retres;
+  __retres = *a;
+  return __retres;
+}
+
+int requires(int volatile *a, int v)
+{
+  *a = v;
+  return v;
+}
+
+/*@ volatile assigns reads ensures writes requires;
+*/
+int slevel = 1000000;
+/*@ lemma bar{L}: slevel ≥ 0;
 
 */
 
-- 
GitLab