Frama-C API - S
The types and function below depend on the abstract domains and values currently available in Eva.
module Analysis : Eva.Analysis.Stype ('env, 'expr, 'v) evaluation_functions = {eval_and_warn : 'env -> 'expr -> 'v * bool * bool;env : Analysis.Dom.t -> Eva.Callstack.t -> '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_functionsval lval_zone_ev : (Analysis.Dom.t, Frama_c_kernel.Cil_types.lval, Frama_c_kernel.Locations.Zone.t) evaluation_functionsval null_ev : (Analysis.Dom.t, unit, Gui_types.gui_offsetmap_res) evaluation_functionsEvaluation 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_functionsval 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_functionsval 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_functionsval 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_functionsval predicate_with_red : Gui_types.gui_loc -> (Eva__.Eval_terms.eval_env * (Frama_c_kernel.Cil_types.kinstr * Eva.Callstack.t), 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_functionsval 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