Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

Signature

module Analysis = X
type ('env, 'expr, 'v) evaluation_functions = {
  1. eval_and_warn : 'env -> 'expr -> 'v * bool * bool;
  2. env : Analysis.Dom.t -> Eva.Callstack.t -> 'env;
  3. equal : 'v -> 'v -> bool;
  4. bottom : 'v;
  5. join : 'v -> 'v -> 'v;
  6. expr_to_gui_selection : 'expr -> Gui_types.gui_selection;
  7. res_to_gui_res : 'expr -> 'v -> Analysis.Val.t Gui_types.gui_res;
}

This is the record that encapsulates all evaluation functions

Evaluation of logic-originating objects is parameterized by a location information, which is used to build the evaluation environment

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