Gui_eval.S
The types and function below depend on the abstract domains and values currently available in Eva.
module Analysis : Eva.Analysis.S
type ('env, 'expr, 'v) evaluation_functions = {
eval_and_warn : 'env -> 'expr -> 'v * bool * bool; |
env : Analysis.Dom.t -> Frama_c_kernel.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 -> Analysis.Val.t Gui_types.gui_res; |
}
This is the record that encapsulates all evaluation functions
val lval_as_offsm_ev :
( Analysis.Dom.t,
Frama_c_kernel.Cil_types.lval,
Gui_types.gui_offsetmap_res )
evaluation_functions
val lval_zone_ev :
( Analysis.Dom.t,
Frama_c_kernel.Cil_types.lval,
Frama_c_kernel.Locations.Zone.t )
evaluation_functions
val null_ev :
( Analysis.Dom.t, unit, Gui_types.gui_offsetmap_res ) 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 ->
( Eva__.Eval_terms.eval_env,
Frama_c_kernel.Cil_types.term,
Gui_types.gui_offsetmap_res )
evaluation_functions
val tlval_zone_ev :
Gui_types.gui_loc ->
( Eva__.Eval_terms.eval_env,
Frama_c_kernel.Cil_types.term,
Frama_c_kernel.Locations.Zone.t )
evaluation_functions
val term_ev :
Gui_types.gui_loc ->
( Eva__.Eval_terms.eval_env,
Frama_c_kernel.Cil_types.term,
Analysis.Val.t Frama_c_kernel.Lattice_bounds.or_bottom )
evaluation_functions
val predicate_ev :
Gui_types.gui_loc ->
( Eva__.Eval_terms.eval_env,
Frama_c_kernel.Cil_types.predicate,
Frama_c_kernel.Abstract_interp.Comp.result
Frama_c_kernel.Lattice_bounds.or_bottom )
evaluation_functions
val predicate_with_red :
Gui_types.gui_loc ->
( Eva__.Eval_terms.eval_env
* (Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Value_types.callstack),
Eva__.Red_statuses.alarm_or_property * Frama_c_kernel.Cil_types.predicate,
Frama_c_kernel.Abstract_interp.Comp.result
Frama_c_kernel.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_selection_data) list * exn list