From c5805536d7f2fb3eec159e06588d3cb1ba84ed55 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 12 Jan 2021 15:31:42 +0100
Subject: [PATCH] [aorai] don't try to show Aorai_curState value for
non-deterministic automaton
---
.../aorai/aorai_eva_analysis.enabled.ml | 20 ++++++++++++-------
1 file changed, 13 insertions(+), 7 deletions(-)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 5b481c60b1d..66770622529 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))
--
GitLab