module type S =sig
..end
The types and function below depend on the abstract domains and values currently available in Eva.
module Analysis:Analysis.S
type ('env, 'expr, 'v)
evaluation_functions = {
|
eval_and_warn : |
|
env : |
|
equal : |
|
bottom : |
|
join : |
|
expr_to_gui_selection : |
|
res_to_gui_res : |
}
This is the record that encapsulates all evaluation functions
val lval_as_offsm_ev : (Analysis.Dom.t, Cil_types.lval, Gui_types.gui_offsetmap_res)
evaluation_functions
val lval_zone_ev : (Analysis.Dom.t, Cil_types.lval, Locations.Zone.t)
evaluation_functions
val null_ev : (Analysis.Dom.t, unit, Gui_types.gui_offsetmap_res)
evaluation_functions
val exp_ev : (Analysis.Dom.t, Cil_types.exp, Analysis.Val.t Lattice_bounds.or_bottom)
evaluation_functions
val lval_ev : (Analysis.Dom.t, Cil_types.lval, Analysis.Val.t Eval.flagged_value)
evaluation_functions
Evaluation of logic-originating objects is parameterized by a location information, which is used to build the evaluation environment
val tlval_ev : Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term, Gui_types.gui_offsetmap_res)
evaluation_functions
val tlval_zone_ev : Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term, Locations.Zone.t)
evaluation_functions
val term_ev : Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.term,
Analysis.Val.t Lattice_bounds.or_bottom)
evaluation_functions
val predicate_ev : Gui_types.gui_loc ->
(Eval_terms.eval_env, Cil_types.predicate,
Eval_terms.predicate_status Lattice_bounds.or_bottom)
evaluation_functions
val predicate_with_red : Gui_types.gui_loc ->
(Eval_terms.eval_env * (Cil_types.kinstr * Value_types.callstack),
Red_statuses.alarm_or_property * Cil_types.predicate,
Eval_terms.predicate_status Lattice_bounds.or_bottom)
evaluation_functions
val make_data_all_callstacks : ('a, 'b, 'c) evaluation_functions ->
Gui_types.gui_loc ->
'b ->
(Gui_types.gui_callstack * Analysis.Val.t Gui_eval.gui_selection_data) list *
exn list