[aorai] take into account observables in backward analysis and spec generation

src/plugins/aorai/aorai_dataflow.ml

@@ -860,42 +860,44 @@ let filter_possible_states kf states =
     treat_one_state post_state Data_for_aorai.Aorai_state.Map.empty
 
 let filter_return_states kf states =
-  let end_state = Return_state.find (Kernel_function.find_return kf) in
-  let auto = Data_for_aorai.getGraph () in
-  let is_possible_state start_state state _ =
-    try
-      let trans = Path_analysis.get_transitions_of_state state auto in
-      let return_states =
-        Data_for_aorai.Aorai_state.Map.find start_state states
-      in
-      let crossable tr =
-        Aorai_utils.isCrossable tr kf Promelaast.Return &&
-        Data_for_aorai.Aorai_state.Map.mem tr.stop return_states
-      in
-      List.exists crossable trans
-    with Not_found -> false
-  in
-  let filter_possible_states state map =
-    Data_for_aorai.Aorai_state.Map.filter (is_possible_state state) map
-  in
-  let treat_one_state state map acc =
-    let res = filter_possible_states state map in
-    if Data_for_aorai.Aorai_state.Map.is_empty res then acc
-    else Data_for_aorai.Aorai_state.Map.add state res acc
-  in
-  let res =
-    Data_for_aorai.Aorai_state.Map.fold
-      treat_one_state end_state Data_for_aorai.Aorai_state.Map.empty
-  in
-  if Data_for_aorai.Aorai_state.Map.is_empty res &&
-     not (Data_for_aorai.Aorai_state.Map.is_empty end_state) then
-    (* Do not emit warning if forward computation already decided that the
-       call was not conforming to the spec. *)
-    Aorai_option.warning ~current:true
-      "Call to %a not conforming to automaton (post-cond). \
-       Assuming it is on a dead path"
-      Kernel_function.pretty kf;
-  res
+  if Data_for_aorai.isObservableFunction kf then begin
+    let end_state = Return_state.find (Kernel_function.find_return kf) in
+    let auto = Data_for_aorai.getGraph () in
+    let is_possible_state start_state state _ =
+      try
+        let trans = Path_analysis.get_transitions_of_state state auto in
+        let return_states =
+          Data_for_aorai.Aorai_state.Map.find start_state states
+        in
+        let crossable tr =
+          Aorai_utils.isCrossable tr kf Promelaast.Return &&
+          Data_for_aorai.Aorai_state.Map.mem tr.stop return_states
+        in
+        List.exists crossable trans
+      with Not_found -> false
+    in
+    let filter_possible_states state map =
+      Data_for_aorai.Aorai_state.Map.filter (is_possible_state state) map
+    in
+    let treat_one_state state map acc =
+      let res = filter_possible_states state map in
+      if Data_for_aorai.Aorai_state.Map.is_empty res then acc
+      else Data_for_aorai.Aorai_state.Map.add state res acc
+    in
+    let res =
+      Data_for_aorai.Aorai_state.Map.fold
+        treat_one_state end_state Data_for_aorai.Aorai_state.Map.empty
+    in
+    if Data_for_aorai.Aorai_state.Map.is_empty res &&
+       not (Data_for_aorai.Aorai_state.Map.is_empty end_state) then
+      (* Do not emit warning if forward computation already decided that the
+         call was not conforming to the spec. *)
+      Aorai_option.warning ~current:true
+        "Call to %a not conforming to automaton (post-cond). \
+         Assuming it is on a dead path"
+        Kernel_function.pretty kf;
+    res
+  end else states
 
 let filter_loop_init_states old_map restrict_map =
   let treat_one_state state old_states acc =

src/plugins/aorai/aorai_visitors.ml

@@ -737,10 +737,12 @@ class visit_adding_pre_post_from_buch treatloops =
             end
           else post_cond
         in
-        let infos = Aorai_utils.get_preds_post_bc_wrt_params kf in
         let post_cond =
-          if Logic_utils.is_trivially_true infos then post_cond
-          else (Normal, Logic_const.new_predicate infos) :: post_cond
+          if Data_for_aorai.isObservableFunction kf then begin
+            let infos = Aorai_utils.get_preds_post_bc_wrt_params kf in
+            if Logic_utils.is_trivially_true infos then post_cond
+            else (Normal, Logic_const.new_predicate infos) :: post_cond
+          end else post_cond
         in
         let post_cond = post_cond @ get_action_post_cond kf return_state in
         [Cil.mk_behavior ~name ~post_cond ()]
@@ -931,9 +933,11 @@ class visit_adding_pre_post_from_buch treatloops =
          let my_state = Data_for_aorai.get_kf_init_state my_kf in
          let requires = needs_zero_one_choice my_state in
          let requires =
-           Aorai_utils.auto_func_preconditions
-             loc my_kf Promelaast.Call my_state
-           @ requires
+           if Data_for_aorai.isObservableFunction my_kf then
+             Aorai_utils.auto_func_preconditions
+               loc my_kf Promelaast.Call my_state
+             @ requires
+           else requires
          in
          let post_cond = needs_post my_kf in
          match Cil.find_default_behavior spec with

src/plugins/aorai/tests/ya/oracle/observed.res.oracle

 [kernel] Parsing tests/ya/observed.i (no preprocessing)
-[aorai] tests/ya/observed.i:15: Warning: 
-  Call to main not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/ya/observed.i:15: Warning: 
-  Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
 [kernel] Parsing TMPDIR/aorai_observed_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
@@ -158,10 +154,7 @@ void f(void)
   return;
 }
 
-/*@ requires \false;
-    
-    behavior Buchi_property_behavior:
-      ensures 1 ≡ first_step ⇒ \false;
+/*@ behavior Buchi_property_behavior:
       ensures
         0 ≡ aorai_intermediate_state ∧
         0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ final ∧ 0 ≡ init;
@@ -309,10 +302,7 @@ void h(void)
   return;
 }
 
-/*@ requires \false;
-    
-    behavior Buchi_property_behavior:
-      ensures 1 ≡ final ⇒ \false;
+/*@ behavior Buchi_property_behavior:
       ensures
         0 ≡ aorai_intermediate_state ∧
         0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ first_step ∧ 0 ≡ init;

src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle

+[kernel] Parsing tests/ya/observed.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_observed_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards