[aorai] Frama_C_show_aorai_state works in non-deterministic state

src/plugins/aorai/aorai_eva_analysis.enabled.ml

@@ -39,13 +39,32 @@ let show_val fmt (expr, v) =
     Printer.pp_exp expr
     (Cvalue.V.pretty_typ (Some (Cil.typeOf expr))) v
 
+let show_non_det_state fmt state =
+  let (states,_) = Data_for_aorai.getGraph () in
+  let first_print = ref true in
+  let print_state s sure =
+    if not !first_print then Format.fprintf fmt ",@ ";
+    first_print := false;
+    Format.fprintf fmt "%s%s"
+      (if sure then "" else "(?)")
+      s.Promelaast.name
+  in
+  let print_one s =
+    (* TODO: sync Data_for_aorai.get_state_var with current project*)
+    let vi = Data_for_aorai.get_varinfo s.Promelaast.name in
+    let e = Cil.evar vi in
+    let cvalue = !Db.Value.eval_expr state e in
+    if Cvalue.V.contains_non_zero cvalue then
+      print_state s (not (Cvalue.V.contains_zero cvalue))
+  in
+  List.iter print_one states
+
 let show_aorai_state = "Frama_C_show_aorai_state"
 
 let builtin_show_aorai_state state args =
   if not (Aorai_option.Deterministic.get()) then begin
-    Aorai_option.warning
-      ~current:true "%s can only display info for deterministic automata"
-      show_aorai_state
+    Aorai_option.result ~current:true
+      "@[<hv 2>Possible states:@ %a@]" show_non_det_state state;
   end else begin
     let history = Data_for_aorai.(curState :: (whole_history ())) in
     Aorai_option.result ~current:true "@[<hv>%a@]"
@@ -77,13 +96,27 @@ let add_slevel_annotation vi kind =
 let add_slevel_annotations () =
   Aorai_visitors.Aux_funcs.iter add_slevel_annotation
 
+let add_nondet_partitioning () =
+  let (states,_) = Data_for_aorai.getGraph() in
+  let add_one_state state =
+    let vi = Data_for_aorai.get_state_var state in
+    Eva.Parameters.use_global_value_partitioning vi
+  in
+  List.iter add_one_state states
+
 let add_partitioning varname =
   match Data_for_aorai.get_varinfo_option varname with
-  | None -> ()
+  | None -> add_nondet_partitioning ()
   | Some vi -> Eva.Parameters.use_global_value_partitioning vi
 
+let add_aux_partitioning () =
+  List.iter
+    Eva.Parameters.use_global_value_partitioning
+    (Data_for_aorai.aux_variables())
+
 let add_state_variables_partitioning () =
   add_partitioning Data_for_aorai.curState;
+  add_aux_partitioning ();
   List.iter add_partitioning (Data_for_aorai.whole_history ())
 
 let setup () =

src/plugins/aorai/tests/ya/observed.i

 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f(void) {}

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

-[kernel] Parsing tests/ya/observed.i (no preprocessing)
+[kernel] Parsing observed.i (no preprocessing)
 [kernel] Parsing TMPDIR/aorai_observed_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {