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 : '-> '-> bool;
    bottom : 'v;
    join : '-> '-> 'v;
    expr_to_gui_selection : 'expr -> Gui_types.gui_selection;
    res_to_gui_res : 'expr -> '-> 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 Cil_types.named,
     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 ->
    '-> 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