sig
val results_kf_computed : Cil_types.kernel_function -> bool
type ('env, 'expr, 'v) evaluation_functions = {
eval_and_warn : 'env -> 'expr -> 'v * bool;
env : Cvalue.Model.t -> Value_types.callstack -> 'env;
equal : 'v -> 'v -> bool;
bottom : 'v;
join : 'v -> 'v -> 'v;
expr_to_gui_selection : 'expr -> Gui_types.gui_selection;
res_to_gui_res : 'expr -> 'v -> Gui_types.gui_res;
}
val lval_ev :
(Cvalue.Model.t, Cil_types.lval, Gui_types.gui_offsetmap_res)
Gui_eval.evaluation_functions
val lval_zone_ev :
(Cvalue.Model.t, Cil_types.lval, Locations.Zone.t)
Gui_eval.evaluation_functions
val null_ev :
(Cvalue.Model.t, unit, Gui_types.gui_offsetmap_res)
Gui_eval.evaluation_functions
val exp_ev :
(Cvalue.Model.t, Cil_types.exp, Cvalue.V.t) Gui_eval.evaluation_functions
val tlval_ev :
Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term, Gui_types.gui_offsetmap_res)
Gui_eval.evaluation_functions
val tlval_zone_ev :
Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term, Locations.Zone.t)
Gui_eval.evaluation_functions
val term_ev :
Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term, Cvalue.V.t)
Gui_eval.evaluation_functions
val predicate_ev :
Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.predicate,
Eval_terms.predicate_status Bottom.or_bottom)
Gui_eval.evaluation_functions
type gui_selection_data = {
alarm : bool;
before : Gui_types.gui_res;
before_string : string Lazy.t;
after : Gui_types.gui_after;
after_string : string Lazy.t;
}
val gui_selection_data_empty : Gui_eval.gui_selection_data
val make_data_all_callstacks :
(Gui_types.gui_selection ->
Gui_types.gui_callstack -> Gui_eval.gui_selection_data -> unit) ->
('a, 'b, 'c) Gui_eval.evaluation_functions ->
before:Cvalue.Model.t Value_types.Callstack.Hashtbl.t ->
after:Cvalue.Model.t Value_types.Callstack.Hashtbl.t option ->
'b -> exn list
val classify_pre_post :
Cil_types.kernel_function -> Property.t -> Gui_types.gui_loc option
type states_by_callstack = {
states_before : Cvalue.Model.t Value_types.Callstack.Hashtbl.t;
states_after : Cvalue.Model.t Value_types.Callstack.Hashtbl.t option;
}
val callstacks_at_gui_loc :
Gui_types.gui_loc -> Gui_eval.states_by_callstack option
val gui_loc_logic_env : Gui_types.gui_loc -> Logic_typing.Lenv.t
end