[aorai] fixes bug in generation of transition functions

when an action is required for a transition in non-deterministic mode, it was
done before the test for updating the boolean variables representing active
state, leading to a possibly incorrect decision when said test depends on the
value of the variable modified by the action

src/plugins/aorai/aorai_utils.ml

@@ -1822,14 +1822,17 @@ let mk_stmt loc (states, tr) f fst status ((st,_) as state) res =
         (List.rev exp_from_trans)
         (List.rev stmt_from_action)
     else
-      List.fold_left2
-        (fun acc cond stmt_act ->
-           if stmt_act = [] then acc
-           else
-             (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
-        [mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt)]
-        (List.rev exp_from_trans)
-        (List.rev stmt_from_action)
+      let actions =
+        List.fold_left2
+          (fun acc cond stmt_act ->
+             if stmt_act = [] then acc
+             else
+               (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
+          []
+          (List.rev exp_from_trans)
+          (List.rev stmt_from_action)
+      in
+      mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
   end else
   if Aorai_option.Deterministic.get () then []
   else [is_out_of_state_stmt state loc]

src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle

@@ -91,15 +91,15 @@ enum aorai_OpStatusList {
     aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
     aorai_intermediate_state_3_tmp = 0;
     aorai_intermediate_state_2_tmp = 0;
-    if (aorai_intermediate_state_0 == 1) 
-      if (aorai_counter < 5) aorai_counter ++;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
     else 
       if (aorai_intermediate_state_0 == 1) 
         if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
         else aorai_intermediate_state_1_tmp = 0;
       else aorai_intermediate_state_1_tmp = 0;
+    if (aorai_intermediate_state_0 == 1) 
+      if (aorai_counter < 5) aorai_counter ++;
+    if (aorai_intermediate_state == 1) aorai_counter = 1;
     aorai_intermediate_state_0_tmp = 0;
     aorai_intermediate_state_tmp = 0;
     Sf_tmp = 0;

src/plugins/aorai/tests/aorai/oracle/seq.res.oracle

@@ -273,10 +273,6 @@ void f(void)
     aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
     aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
     aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
-    if (aorai_intermediate_state_2 == 1) 
-      if (aorai_counter < 2) aorai_counter ++;
-    if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1;
     else 
       if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1;
@@ -285,6 +281,10 @@ void f(void)
           if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
           else aorai_intermediate_state_3_tmp = 0;
         else aorai_intermediate_state_3_tmp = 0;
+    if (aorai_intermediate_state_2 == 1) 
+      if (aorai_counter < 2) aorai_counter ++;
+    if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
+    if (aorai_intermediate_state == 1) aorai_counter = 1;
     aorai_intermediate_state_2_tmp = 0;
     aorai_intermediate_state_1_tmp = 0;
     aorai_intermediate_state_0_tmp = 0;

src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle

@@ -91,15 +91,15 @@ enum aorai_OpStatusList {
     aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
     aorai_intermediate_state_3_tmp = 0;
     aorai_intermediate_state_2_tmp = 0;
-    if (aorai_intermediate_state_0 == 1) 
-      if (aorai_counter < 5) aorai_counter ++;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
     else 
       if (aorai_intermediate_state_0 == 1) 
         if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
         else aorai_intermediate_state_1_tmp = 0;
       else aorai_intermediate_state_1_tmp = 0;
+    if (aorai_intermediate_state_0 == 1) 
+      if (aorai_counter < 5) aorai_counter ++;
+    if (aorai_intermediate_state == 1) aorai_counter = 1;
     aorai_intermediate_state_0_tmp = 0;
     aorai_intermediate_state_tmp = 0;
     Sf_tmp = 0;

src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle

@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func

src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle

@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_3 in automaton function g_pre_func

src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle

@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func