diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml index b0b1538a7e793a70adf5bd676bdccf1c9cfb9893..47322653a793c501b984534b3ecdb61ab75449f7 100644 --- a/src/plugins/value/gui_files/gui_red.ml +++ b/src/plugins/value/gui_files/gui_red.ml @@ -60,9 +60,6 @@ type red_alarm = { function_name:string; kind:string; acsl: string; - alarm_or_prop: Red_statuses.alarm_or_property; - (* Status here means 'final' status as emitted by all plugins. Currentlt not - shown. *) ip: Property.t; callstacks: int; (* Number of callstacks in which the red alarm occured. *) } @@ -88,14 +85,12 @@ let make_red_alarm function_name ki alarm callstacks = let acsl = Format.asprintf "@[<hov>%a@]" Cil_datatype.Toplevel_predicate.pretty p in - let alarm_or_prop = Red_statuses.Alarm alarm in - { function_name; ip; kind; alarm_or_prop; acsl; callstacks } + { function_name; ip; kind; acsl; callstacks } let make_red_prop function_name ip callstacks = let kind = "property" (* TODO *) in let acsl = Format.asprintf "@[<hov>%a@]" Property.pretty ip in - let alarm_or_prop = Red_statuses.Prop ip in - { function_name; ip; kind; alarm_or_prop; acsl; callstacks } + { function_name; ip; kind; acsl; callstacks } diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml index 548914728a9fd2684cfa7e5f0ab279a49da795b6..5d1d845e294d1fcac34816b8f2821c8cf04ba20f 100644 --- a/src/plugins/value/utils/value_perf.ml +++ b/src/plugins/value/utils/value_perf.ml @@ -47,10 +47,6 @@ module Call_info = struct (* How many times the function was called. *) mutable nb_calls: int; - (* How many times the call had to be computed (i.e. with calls - cached with memexec removed) *) - mutable nb_effective_calls: int; - (* The accumulated execution time for past calls. *) mutable total_duration: float; @@ -60,8 +56,7 @@ module Call_info = struct } ;; - let create() = { nb_calls = 0; nb_effective_calls = 0; total_duration = 0.0; - since = [] };; + let create() = { nb_calls = 0; total_duration = 0.0; since = [] };; (* Represents the calls to the main function. *) let main = create();; @@ -342,7 +337,6 @@ let stop_doing_perf callstack = let reset_perf () = let reset_callinfo ci = ci.Call_info.nb_calls <- 0; - ci.Call_info.nb_effective_calls <- 0; ci.Call_info.total_duration <- 0.0; ci.Call_info.since <- [] in