From dbb2f5c6a92874ed1cd23ff2d3f751d7c6d13385 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sun, 26 Dec 2021 12:08:43 +0100
Subject: [PATCH] [aorai] fix contract of unobserved functions called in
 several contexts

---
 src/plugins/aorai/aorai_visitors.ml           |  6 +++-
 .../aorai/tests/ya/oracle/observed.res.oracle | 31 ++++++++++++++++---
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 9d4ddad0f1b..aadd8a359bd 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -398,7 +398,11 @@ let possible_start kf (start,int) =
     Logic_const.por
       (cond, Aorai_utils.crosscond_to_pred tr.cross kf Promelaast.Call)
   in
-  let cond = List.fold_left treat_one_trans Logic_const.pfalse trans in
+  let cond =
+    if Data_for_aorai.isObservableFunction kf then
+      List.fold_left treat_one_trans Logic_const.pfalse trans
+    else Logic_const.ptrue
+  in
   Logic_const.pand (Aorai_utils.is_state_pred start, cond)
 
 let neg_trans kf trans =
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 986a6bd390b..4e5eac6d384 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -154,11 +154,32 @@ void f(void)
   return;
 }
 
-/*@ behavior Buchi_property_behavior:
-      ensures
-        0 ≡ aorai_intermediate_state ∧
-        0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ final ∧ 0 ≡ init;
+/*@ requires 1 ≡ first_step ∨ 0 ≡ first_step;
+    requires
+      1 ≡ aorai_intermediate_state_0 ∨ 0 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_in_0:
+      assumes 1 ≡ aorai_intermediate_state_0;
+      ensures 1 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_in_1:
+      assumes 1 ≡ first_step;
       ensures 1 ≡ first_step;
+    
+    behavior Buchi_behavior_out_0:
+      ensures 0 ≡ aorai_intermediate_state;
+    
+    behavior Buchi_behavior_out_1:
+      ensures 0 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_out_2:
+      ensures 0 ≡ final;
+    
+    behavior Buchi_behavior_out_3:
+      ensures 0 ≡ first_step;
+    
+    behavior Buchi_behavior_out_4:
+      ensures 0 ≡ init;
  */
 void g(void)
 {
@@ -298,6 +319,8 @@ void g(void)
 void h(void)
 {
   /*@ ghost h_pre_func(); */
+  g();
+  g();
   /*@ ghost h_post_func(); */
   return;
 }
-- 
GitLab