[tests] update ACSL kw test and oracles

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;

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:

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;
 
 */