From 544344c972d442f7c7e1ad8d0a1dd4cf7b367052 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Apr 2020 15:13:51 +0200
Subject: [PATCH] [aorai] validate oracles

---
 .../aorai/tests/aorai/oracle/formals.res.oracle    | 14 ++++++++------
 .../aorai/tests/aorai/oracle/other.res.oracle      | 10 ++++++++--
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
index 2e24eb7f8a7..b850086cbe9 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
@@ -581,24 +581,26 @@ int g(int y)
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+        aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+        aorai_x_0 ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+        aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+        aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+        aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+        aorai_x_0 ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+        aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+        aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
  */
 int main(void)
 {
diff --git a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
index 91b4e2cc2ad..480cdbac3e3 100644
--- a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
@@ -525,7 +525,12 @@ void g(void)
      behavior buch_state_last_out:
        ensures 0 ≡ last;
      
+     behavior buch_state_step1_in:
+       assumes 1 ≡ init ∧ x ≡ 3;
+       ensures 1 ≡ step1;
+     
      behavior buch_state_step1_out:
+       assumes 0 ≡ init ∨ ¬(x ≡ 3);
        ensures 0 ≡ step1;
    @/
   void main_pre_func(void)
@@ -538,7 +543,9 @@ void g(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    step1_tmp = 0;
+    if (init == 1) 
+      if (x == 3) step1_tmp = 1; else step1_tmp = 0;
+    else step1_tmp = 0;
     last_tmp = 0;
     if (init == 1) 
       if (x != 3) init_tmp = 1; else init_tmp = 0;
@@ -644,7 +651,6 @@ void g(void)
 */
 
 /*@ requires 1 ≡ init ∧ 0 ≡ last ∧ 0 ≡ step1;
-    requires 1 ≡ init ⇒ x ≢ 3;
     
     behavior aorai_acceptance:
       ensures 1 ≡ last;
-- 
GitLab