diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml index 5b481c60b1d80bc9c1132323a5f88d2ea80b63ae..6677062252912351507f77c28f5e9a6ae6e0851a 100644 --- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml +++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml @@ -39,13 +39,21 @@ let show_val fmt (expr, v, _) = Printer.pp_exp expr (Cvalue.V.pretty_typ (Some (Cil.typeOf expr))) v +let show_aorai_state = "Frama_C_show_aorai_state" + let builtin_show_aorai_state state args = - let history = Data_for_aorai.(curState :: (whole_history ())) in - Aorai_option.result ~current:true "@[<hv>%a@]" - (Pretty_utils.pp_list ~sep:" <- " (show_aorai_variable state)) history; - if args <> [] then begin + if not (Aorai_option.Deterministic.get()) then begin + Aorai_option.warning + ~current:true "%s can only display info for deterministic automata" + show_aorai_state + end else begin + let history = Data_for_aorai.(curState :: (whole_history ())) in Aorai_option.result ~current:true "@[<hv>%a@]" - (Pretty_utils.pp_list ~sep:"," show_val) args + (Pretty_utils.pp_list ~sep:" <- " (show_aorai_variable state)) history; + if args <> [] then begin + Aorai_option.result ~current:true "@[<hv>%a@]" + (Pretty_utils.pp_list ~sep:"," show_val) args + end; end; (* Return value : returns nothing, changes nothing *) { @@ -55,8 +63,6 @@ let builtin_show_aorai_state state args = c_cacheable = Value_types.Cacheable; } -let show_aorai_state = "Frama_C_show_aorai_state" - let () = Cil_builtins.add_custom_builtin (fun () -> (show_aorai_state,Cil.voidType,[],true))