sig
  val results_kf_computed : Cil_types.kernel_function -> bool
  val classify_pre_post :
    Cil_types.kernel_function -> Property.t -> Gui_types.gui_loc option
  val gui_loc_logic_env : Gui_types.gui_loc -> Logic_typing.Lenv.t
  type 'a gui_selection_data = {
    alarm : bool;
    red : bool;
    before : 'Gui_types.gui_res;
    before_string : string Stdlib.Lazy.t;
    after : 'Gui_types.gui_after;
    after_string : string Stdlib.Lazy.t;
  }
  val gui_selection_data_empty : 'Gui_eval.gui_selection_data
  module type S =
    sig
      module Analysis : Analysis.S
      type ('env, 'expr, 'v) evaluation_functions = {
        eval_and_warn : 'env -> 'expr -> 'v * bool * bool;
        env : Analysis.Dom.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 -> '-> Analysis.Val.t Gui_types.gui_res;
      }
      val lval_as_offsm_ev :
        (Analysis.Dom.t, Cil_types.lval, Gui_types.gui_offsetmap_res)
        Gui_eval.S.evaluation_functions
      val lval_zone_ev :
        (Analysis.Dom.t, Cil_types.lval, Locations.Zone.t)
        Gui_eval.S.evaluation_functions
      val null_ev :
        (Analysis.Dom.t, unit, Gui_types.gui_offsetmap_res)
        Gui_eval.S.evaluation_functions
      val exp_ev :
        (Analysis.Dom.t, Cil_types.exp, Analysis.Val.t Bottom.or_bottom)
        Gui_eval.S.evaluation_functions
      val lval_ev :
        (Analysis.Dom.t, Cil_types.lval, Analysis.Val.t Eval.flagged_value)
        Gui_eval.S.evaluation_functions
      val tlval_ev :
        Gui_types.gui_loc ->
        (Eval_terms.eval_env, Cil_types.term, Gui_types.gui_offsetmap_res)
        Gui_eval.S.evaluation_functions
      val tlval_zone_ev :
        Gui_types.gui_loc ->
        (Eval_terms.eval_env, Cil_types.term, Locations.Zone.t)
        Gui_eval.S.evaluation_functions
      val term_ev :
        Gui_types.gui_loc ->
        (Eval_terms.eval_env, Cil_types.term,
         Analysis.Val.t Bottom.or_bottom)
        Gui_eval.S.evaluation_functions
      val predicate_ev :
        Gui_types.gui_loc ->
        (Eval_terms.eval_env, Cil_types.predicate,
         Eval_terms.predicate_status Bottom.or_bottom)
        Gui_eval.S.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 Bottom.or_bottom)
        Gui_eval.S.evaluation_functions
      val make_data_all_callstacks :
        ('a, 'b, 'c) Gui_eval.S.evaluation_functions ->
        Gui_types.gui_loc ->
        '->
        (Gui_types.gui_callstack * Analysis.Val.t Gui_eval.gui_selection_data)
        list * exn list
    end
  module Make :
    functor (X : Analysis.S->
      sig
        module Analysis :
          sig
            module Val :
              sig
                type t = X.Val.t
                val ty : t Type.t
                val name : string
                val descr : t Descr.t
                val packed_descr : Structural_descr.pack
                val reprs : t list
                val equal : t -> t -> bool
                val compare : t -> t -> int
                val hash : t -> int
                val pretty_code : Format.formatter -> t -> unit
                val internal_pretty_code :
                  Type.precedence -> Format.formatter -> t -> unit
                val pretty : Format.formatter -> t -> unit
                val varname : t -> string
                val mem_project : (Project_skeleton.t -> bool) -> t -> bool
                val copy : t -> t
                val pretty_typ :
                  Cil_types.typ option -> t Pretty_utils.formatter
                val top : t
                val is_included : t -> t -> bool
                val join : t -> t -> t
                val narrow : t -> t -> t Eval.or_bottom
                val zero : t
                val one : t
                val top_int : t
                val inject_int : Cil_types.typ -> Integer.t -> t
                val assume_non_zero : t -> t Abstract_value.truth
                val assume_bounded :
                  Abstract_value.bound_kind ->
                  Abstract_value.bound -> t -> t Abstract_value.truth
                val assume_not_nan :
                  assume_finite:bool ->
                  Cil_types.fkind -> t -> t Abstract_value.truth
                val assume_pointer : t -> t Abstract_value.truth
                val assume_comparable :
                  Abstract_value.pointer_comparison ->
                  t -> t -> (t * t) Abstract_value.truth
                val constant : Cil_types.exp -> Cil_types.constant -> t
                val forward_unop :
                  Cil_types.typ -> Cil_types.unop -> t -> t Eval.or_bottom
                val forward_binop :
                  Cil_types.typ ->
                  Cil_types.binop -> t -> t -> t Eval.or_bottom
                val rewrap_integer : Eval_typ.integer_range -> t -> t
                val forward_cast :
                  src_type:Eval_typ.scalar_typ ->
                  dst_type:Eval_typ.scalar_typ -> t -> t Eval.or_bottom
                val backward_binop :
                  input_type:Cil_types.typ ->
                  resulting_type:Cil_types.typ ->
                  Cil_types.binop ->
                  left:t ->
                  right:t -> result:t -> (t option * t option) Eval.or_bottom
                val backward_unop :
                  typ_arg:Cil_types.typ ->
                  Cil_types.unop -> arg:t -> res:t -> t option Eval.or_bottom
                val backward_cast :
                  src_typ:Cil_types.typ ->
                  dst_typ:Cil_types.typ ->
                  src_val:t -> dst_val:t -> t option Eval.or_bottom
                val resolve_functions :
                  t -> Kernel_function.t list Eval.or_top * bool
                val replace_base : Base.substitution -> t -> t
                val structure : t Abstract.Value.structure
                val mem : 'Abstract.Value.key -> bool
                val get : 'Abstract.Value.key -> (t -> 'a) option
                val set : 'Abstract.Value.key -> '-> t -> t
                val reduce : t -> t
              end
            module Loc :
              sig
                type value = Val.t
                type location = X.Loc.location
                type offset = X.Loc.offset
                val top : location
                val equal_loc : location -> location -> bool
                val equal_offset : offset -> offset -> bool
                val pretty_loc : Format.formatter -> location -> unit
                val pretty_offset : Format.formatter -> offset -> unit
                val to_value : location -> value
                val size : location -> Int_Base.t
                val replace_base : Base.substitution -> location -> location
                val assume_no_overlap :
                  partial:bool ->
                  location ->
                  location -> (location * location) Abstract_location.truth
                val assume_valid_location :
                  for_writing:bool ->
                  bitfield:bool ->
                  location -> location Abstract_location.truth
                val no_offset : offset
                val forward_field :
                  Cil_types.typ -> Cil_types.fieldinfo -> offset -> offset
                val forward_index :
                  Cil_types.typ -> value -> offset -> offset
                val forward_variable :
                  Cil_types.typ ->
                  Cil_types.varinfo -> offset -> location Eval.or_bottom
                val forward_pointer :
                  Cil_types.typ -> value -> offset -> location Eval.or_bottom
                val eval_varinfo : Cil_types.varinfo -> location
                val backward_variable :
                  Cil_types.varinfo -> location -> offset Eval.or_bottom
                val backward_pointer :
                  value ->
                  offset -> location -> (value * offset) Eval.or_bottom
                val backward_field :
                  Cil_types.typ ->
                  Cil_types.fieldinfo -> offset -> offset Eval.or_bottom
                val backward_index :
                  Cil_types.typ ->
                  index:value ->
                  remaining:offset ->
                  offset -> (value * offset) Eval.or_bottom
                val structure : location Abstract.Location.structure
                val mem : 'Abstract.Location.key -> bool
                val get : 'Abstract.Location.key -> (location -> 'a) option
                val set :
                  'Abstract.Location.key -> '-> location -> location
              end
            module Dom :
              sig
                type state = X.Dom.state
                type t = state
                val ty : t Type.t
                val name : string
                val descr : t Descr.t
                val packed_descr : Structural_descr.pack
                val reprs : t list
                val equal : t -> t -> bool
                val compare : t -> t -> int
                val hash : t -> int
                val pretty_code : Format.formatter -> t -> unit
                val internal_pretty_code :
                  Type.precedence -> Format.formatter -> t -> unit
                val pretty : Format.formatter -> t -> unit
                val varname : t -> string
                val mem_project : (Project_skeleton.t -> bool) -> t -> bool
                val copy : t -> t
                module Set :
                  sig
                    type elt = t
                    type t = X.Dom.Set.t
                    val empty : t
                    val is_empty : t -> bool
                    val mem : elt -> t -> bool
                    val add : elt -> t -> t
                    val singleton : elt -> t
                    val remove : elt -> t -> t
                    val union : t -> t -> t
                    val inter : t -> t -> t
                    val disjoint : t -> t -> bool
                    val diff : t -> t -> t
                    val subset : t -> t -> bool
                    val iter : (elt -> unit) -> t -> unit
                    val map : (elt -> elt) -> t -> t
                    val fold : (elt -> '-> 'a) -> t -> '-> 'a
                    val for_all : (elt -> bool) -> t -> bool
                    val exists : (elt -> bool) -> t -> bool
                    val filter : (elt -> bool) -> t -> t
                    val filter_map : (elt -> elt option) -> t -> t
                    val partition : (elt -> bool) -> t -> t * t
                    val cardinal : t -> int
                    val elements : t -> elt list
                    val min_elt : t -> elt
                    val min_elt_opt : t -> elt option
                    val max_elt : t -> elt
                    val max_elt_opt : t -> elt option
                    val choose : t -> elt
                    val choose_opt : t -> elt option
                    val split : elt -> t -> t * bool * t
                    val find : elt -> t -> elt
                    val find_opt : elt -> t -> elt option
                    val find_first : (elt -> bool) -> t -> elt
                    val find_first_opt : (elt -> bool) -> t -> elt option
                    val find_last : (elt -> bool) -> t -> elt
                    val find_last_opt : (elt -> bool) -> t -> elt option
                    val of_list : elt list -> t
                    val to_seq_from : elt -> t -> elt Seq.t
                    val to_seq : t -> elt Seq.t
                    val add_seq : elt Seq.t -> t -> t
                    val of_seq : elt Seq.t -> t
                    val nearest_elt_le : elt -> t -> elt
                    val nearest_elt_ge : elt -> t -> elt
                    val ty : t Type.t
                    val name : string
                    val descr : t Descr.t
                    val packed_descr : Structural_descr.pack
                    val reprs : t list
                    val equal : t -> t -> bool
                    val compare : t -> t -> int
                    val hash : t -> int
                    val pretty_code : Format.formatter -> t -> unit
                    val internal_pretty_code :
                      Type.precedence -> Format.formatter -> t -> unit
                    val pretty : Format.formatter -> t -> unit
                    val varname : t -> string
                    val mem_project :
                      (Project_skeleton.t -> bool) -> t -> bool
                    val copy : t -> t
                  end
                module Map :
                  sig
                    type key = t
                    type 'a t = 'X.Dom.Map.t
                    val empty : 'a t
                    val is_empty : 'a t -> bool
                    val mem : key -> 'a t -> bool
                    val add : key -> '-> 'a t -> 'a t
                    val update :
                      key -> ('a option -> 'a option) -> 'a t -> 'a t
                    val singleton : key -> '-> 'a t
                    val remove : key -> 'a t -> 'a t
                    val merge :
                      (key -> 'a option -> 'b option -> 'c option) ->
                      'a t -> 'b t -> 'c t
                    val union :
                      (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
                    val compare : ('-> '-> int) -> 'a t -> 'a t -> int
                    val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
                    val iter : (key -> '-> unit) -> 'a t -> unit
                    val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                    val for_all : (key -> '-> bool) -> 'a t -> bool
                    val exists : (key -> '-> bool) -> 'a t -> bool
                    val filter : (key -> '-> bool) -> 'a t -> 'a t
                    val filter_map : (key -> '-> 'b option) -> 'a t -> 'b t
                    val partition :
                      (key -> '-> bool) -> 'a t -> 'a t * 'a t
                    val cardinal : 'a t -> int
                    val bindings : 'a t -> (key * 'a) list
                    val min_binding : 'a t -> key * 'a
                    val min_binding_opt : 'a t -> (key * 'a) option
                    val max_binding : 'a t -> key * 'a
                    val max_binding_opt : 'a t -> (key * 'a) option
                    val choose : 'a t -> key * 'a
                    val choose_opt : 'a t -> (key * 'a) option
                    val split : key -> 'a t -> 'a t * 'a option * 'a t
                    val find : key -> 'a t -> 'a
                    val find_opt : key -> 'a t -> 'a option
                    val find_first : (key -> bool) -> 'a t -> key * 'a
                    val find_first_opt :
                      (key -> bool) -> 'a t -> (key * 'a) option
                    val find_last : (key -> bool) -> 'a t -> key * 'a
                    val find_last_opt :
                      (key -> bool) -> 'a t -> (key * 'a) option
                    val map : ('-> 'b) -> 'a t -> 'b t
                    val mapi : (key -> '-> 'b) -> 'a t -> 'b t
                    val to_seq : 'a t -> (key * 'a) Seq.t
                    val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
                    val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
                    val of_seq : (key * 'a) Seq.t -> 'a t
                    module Key :
                      sig
                        type t = key
                        val ty : t Type.t
                        val name : string
                        val descr : t Descr.t
                        val packed_descr : Structural_descr.pack
                        val reprs : t list
                        val equal : t -> t -> bool
                        val compare : t -> t -> int
                        val hash : t -> int
                        val pretty_code : Format.formatter -> t -> unit
                        val internal_pretty_code :
                          Type.precedence -> Format.formatter -> t -> unit
                        val pretty : Format.formatter -> t -> unit
                        val varname : t -> string
                        val mem_project :
                          (Project_skeleton.t -> bool) -> t -> bool
                        val copy : t -> t
                      end
                    module Make :
                      functor (Data : Datatype.S->
                        sig
                          type t = Data.t t
                          val ty : t Type.t
                          val name : string
                          val descr : t Descr.t
                          val packed_descr : Structural_descr.pack
                          val reprs : t list
                          val equal : t -> t -> bool
                          val compare : t -> t -> int
                          val hash : t -> int
                          val pretty_code : Format.formatter -> t -> unit
                          val internal_pretty_code :
                            Type.precedence -> Format.formatter -> t -> unit
                          val pretty : Format.formatter -> t -> unit
                          val varname : t -> string
                          val mem_project :
                            (Project_skeleton.t -> bool) -> t -> bool
                          val copy : t -> t
                        end
                  end
                module Hashtbl :
                  sig
                    type key = t
                    type 'a t = 'X.Dom.Hashtbl.t
                    val create : int -> 'a t
                    val clear : 'a t -> unit
                    val reset : 'a t -> unit
                    val copy : 'a t -> 'a t
                    val add : 'a t -> key -> '-> unit
                    val remove : 'a t -> key -> unit
                    val find : 'a t -> key -> 'a
                    val find_all : 'a t -> key -> 'a list
                    val replace : 'a t -> key -> '-> unit
                    val mem : 'a t -> key -> bool
                    val iter : (key -> '-> unit) -> 'a t -> unit
                    val filter_map_inplace :
                      (key -> '-> 'a option) -> 'a t -> unit
                    val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                    val length : 'a t -> int
                    val stats : 'a t -> Hashtbl.statistics
                    val to_seq : 'a t -> (key * 'a) Seq.t
                    val to_seq_keys : 'a t -> key Seq.t
                    val to_seq_values : 'a t -> 'Seq.t
                    val add_seq : 'a t -> (key * 'a) Seq.t -> unit
                    val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
                    val of_seq : (key * 'a) Seq.t -> 'a t
                    val iter_sorted :
                      ?cmp:(key -> key -> int) ->
                      (key -> '-> unit) -> 'a t -> unit
                    val fold_sorted :
                      ?cmp:(key -> key -> int) ->
                      (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                    val iter_sorted_by_entry :
                      cmp:(key * '-> key * '-> int) ->
                      (key -> '-> unit) -> 'a t -> unit
                    val fold_sorted_by_entry :
                      cmp:(key * '-> key * '-> int) ->
                      (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                    val iter_sorted_by_value :
                      cmp:('-> '-> int) ->
                      (key -> '-> unit) -> 'a t -> unit
                    val fold_sorted_by_value :
                      cmp:('-> '-> int) ->
                      (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                    val find_opt : 'a t -> key -> 'a option
                    val find_def : 'a t -> key -> '-> 'a
                    val memo : 'a t -> key -> (key -> 'a) -> 'a
                    val structural_descr :
                      Structural_descr.t -> Structural_descr.t
                    val make_type : 'Type.t -> 'a t Type.t
                    module Key :
                      sig
                        type t = key
                        val ty : t Type.t
                        val name : string
                        val descr : t Descr.t
                        val packed_descr : Structural_descr.pack
                        val reprs : t list
                        val equal : t -> t -> bool
                        val compare : t -> t -> int
                        val hash : t -> int
                        val pretty_code : Format.formatter -> t -> unit
                        val internal_pretty_code :
                          Type.precedence -> Format.formatter -> t -> unit
                        val pretty : Format.formatter -> t -> unit
                        val varname : t -> string
                        val mem_project :
                          (Project_skeleton.t -> bool) -> t -> bool
                        val copy : t -> t
                      end
                    module Make :
                      functor (Data : Datatype.S->
                        sig
                          type t = Data.t t
                          val ty : t Type.t
                          val name : string
                          val descr : t Descr.t
                          val packed_descr : Structural_descr.pack
                          val reprs : t list
                          val equal : t -> t -> bool
                          val compare : t -> t -> int
                          val hash : t -> int
                          val pretty_code : Format.formatter -> t -> unit
                          val internal_pretty_code :
                            Type.precedence -> Format.formatter -> t -> unit
                          val pretty : Format.formatter -> t -> unit
                          val varname : t -> string
                          val mem_project :
                            (Project_skeleton.t -> bool) -> t -> bool
                          val copy : t -> t
                        end
                  end
                val top : t
                val is_included : t -> t -> bool
                val join : t -> t -> t
                val widen :
                  Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
                val narrow : t -> t -> t Eval.or_bottom
                type value = Val.t
                type location = Loc.location
                type origin = X.Dom.origin
                val extract_expr :
                  oracle:(Cil_types.exp -> value Eval.evaluated) ->
                  Abstract_domain.evaluation_context ->
                  t ->
                  Cil_types.exp -> (value * origin option) Eval.evaluated
                val extract_lval :
                  oracle:(Cil_types.exp -> value Eval.evaluated) ->
                  Abstract_domain.evaluation_context ->
                  t ->
                  Cil_types.lval ->
                  Cil_types.typ ->
                  location -> (value * origin option) Eval.evaluated
                val backward_location :
                  t ->
                  Cil_types.lval ->
                  Cil_types.typ ->
                  location -> value -> (location * value) Eval.or_bottom
                val reduce_further :
                  t -> Cil_types.exp -> value -> (Cil_types.exp * value) list
                val update :
                  (value, location, origin) Abstract_domain.valuation ->
                  t -> t Eval.or_bottom
                val assign :
                  Cil_types.kinstr ->
                  location Eval.left_value ->
                  Cil_types.exp ->
                  (location, value) Eval.assigned ->
                  (value, location, origin) Abstract_domain.valuation ->
                  t -> t Eval.or_bottom
                val assume :
                  Cil_types.stmt ->
                  Cil_types.exp ->
                  bool ->
                  (value, location, origin) Abstract_domain.valuation ->
                  t -> t Eval.or_bottom
                val start_call :
                  Cil_types.stmt ->
                  (location, value) Eval.call ->
                  Eval.recursion option ->
                  (value, location, origin) Abstract_domain.valuation ->
                  t -> t Eval.or_bottom
                val finalize_call :
                  Cil_types.stmt ->
                  (location, value) Eval.call ->
                  Eval.recursion option ->
                  pre:t -> post:t -> t Eval.or_bottom
                val show_expr :
                  (value, location, origin) Abstract_domain.valuation ->
                  t -> Format.formatter -> Cil_types.exp -> unit
                val logic_assign :
                  (location Eval.logic_assign * state) option ->
                  location -> state -> state
                val evaluate_predicate :
                  state Abstract_domain.logic_environment ->
                  state -> Cil_types.predicate -> Alarmset.status
                val reduce_by_predicate :
                  state Abstract_domain.logic_environment ->
                  state ->
                  Cil_types.predicate -> bool -> state Eval.or_bottom
                val enter_scope :
                  Abstract_domain.variable_kind ->
                  Cil_types.varinfo list -> t -> t
                val leave_scope :
                  Cil_types.kernel_function ->
                  Cil_types.varinfo list -> t -> t
                val empty : unit -> t
                val initialize_variable :
                  Cil_types.lval ->
                  location ->
                  initialized:bool -> Abstract_domain.init_value -> t -> t
                val initialize_variable_using_type :
                  Abstract_domain.variable_kind ->
                  Cil_types.varinfo -> t -> t
                val enter_loop : Cil_types.stmt -> state -> state
                val incr_loop_counter : Cil_types.stmt -> state -> state
                val leave_loop : Cil_types.stmt -> state -> state
                val relate :
                  Cil_types.kernel_function ->
                  Base.Hptset.t -> t -> Base.SetLattice.t
                val filter :
                  Cil_types.kernel_function ->
                  [ `Post | `Pre ] -> Base.Hptset.t -> t -> t
                val reuse :
                  Cil_types.kernel_function ->
                  Base.Hptset.t -> current_input:t -> previous_output:t -> t
                val log_category : Value_parameters.category
                module Store :
                  sig
                    val register_global_state : state Eval.or_bottom -> unit
                    val register_initial_state :
                      Value_types.callstack -> state -> unit
                    val register_state_before_stmt :
                      Value_types.callstack ->
                      Cil_types.stmt -> state -> unit
                    val register_state_after_stmt :
                      Value_types.callstack ->
                      Cil_types.stmt -> state -> unit
                    val get_global_state : unit -> state Eval.or_bottom
                    val get_initial_state :
                      Cil_types.kernel_function -> state Eval.or_bottom
                    val get_initial_state_by_callstack :
                      Cil_types.kernel_function ->
                      state Value_types.Callstack.Hashtbl.t
                      Eval.or_top_or_bottom
                    val get_stmt_state :
                      after:bool -> Cil_types.stmt -> state Eval.or_bottom
                    val get_stmt_state_by_callstack :
                      after:bool ->
                      Cil_types.stmt ->
                      state Value_types.Callstack.Hashtbl.t
                      Eval.or_top_or_bottom
                  end
                val post_analysis : t Eval.or_bottom -> unit
                val structure : t Abstract.Domain.structure
                val mem : 'Abstract.Domain.key -> bool
                val get : 'Abstract.Domain.key -> (t -> 'a) option
                val set : 'Abstract.Domain.key -> '-> t -> t
                val get_cvalue : (t -> Cvalue.Model.t) option
                val get_cvalue_or_top : t -> Cvalue.Model.t
                val get_cvalue_or_bottom :
                  t Bottom.or_bottom -> Cvalue.Model.t
              end
            module Eval :
              sig
                type state = Dom.t
                type value = Val.t
                type origin = Dom.origin
                type loc = Loc.location
                module Valuation :
                  sig
                    type t = X.Eval.Valuation.t
                    type value = value
                    type origin = origin
                    type loc = loc
                    val empty : t
                    val find :
                      t ->
                      Cil_types.exp ->
                      (value, origin) Eval.record_val Eval.or_top
                    val add :
                      t ->
                      Cil_types.exp -> (value, origin) Eval.record_val -> t
                    val fold :
                      (Cil_types.exp ->
                       (value, origin) Eval.record_val -> '-> 'a) ->
                      t -> '-> 'a
                    val find_loc :
                      t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top
                    val remove : t -> Cil_types.exp -> t
                    val remove_loc : t -> Cil_types.lval -> t
                  end
                val to_domain_valuation :
                  Valuation.t ->
                  (value, loc, origin) Abstract_domain.valuation
                val evaluate :
                  ?valuation:Valuation.t ->
                  ?reduction:bool ->
                  ?subdivnb:int ->
                  state ->
                  Cil_types.exp -> (Valuation.t * value) Eval.evaluated
                val copy_lvalue :
                  ?valuation:Valuation.t ->
                  ?subdivnb:int ->
                  state ->
                  Cil_types.lval ->
                  (Valuation.t * value Eval.flagged_value) Eval.evaluated
                val lvaluate :
                  ?valuation:Valuation.t ->
                  ?subdivnb:int ->
                  for_writing:bool ->
                  state ->
                  Cil_types.lval ->
                  (Valuation.t * loc * Cil_types.typ) Eval.evaluated
                val reduce :
                  ?valuation:Valuation.t ->
                  state ->
                  Cil_types.exp -> bool -> Valuation.t Eval.evaluated
                val assume :
                  ?valuation:Valuation.t ->
                  state ->
                  Cil_types.exp -> value -> Valuation.t Eval.or_bottom
                val eval_function_exp :
                  ?subdivnb:int ->
                  Cil_types.exp ->
                  ?args:Cil_types.exp list ->
                  state ->
                  (Kernel_function.t * Valuation.t) list Eval.evaluated
                val interpret_truth :
                  alarm:(unit -> Alarms.t) ->
                  '-> 'Abstract_value.truth -> 'Eval.evaluated
              end
            val get_stmt_state :
              after:bool -> Cil_types.stmt -> Dom.state Eval.or_bottom
            val get_kinstr_state :
              after:bool -> Cil_types.kinstr -> Dom.state Eval.or_bottom
            val get_stmt_state_by_callstack :
              after:bool ->
              Cil_types.stmt ->
              Dom.state Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom
            val get_initial_state_by_callstack :
              Cil_types.kernel_function ->
              Dom.state Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom
            val eval_expr :
              Dom.state -> Cil_types.exp -> Val.t Eval.evaluated
            val copy_lvalue :
              Dom.state ->
              Cil_types.lval -> Val.t Eval.flagged_value Eval.evaluated
            val eval_lval_to_loc :
              Dom.state -> Cil_types.lval -> Loc.location Eval.evaluated
            val eval_function_exp :
              Dom.state ->
              ?args:Cil_types.exp list ->
              Cil_types.exp -> Cil_types.kernel_function list Eval.evaluated
            val assume_cond :
              Cil_types.stmt ->
              Dom.state -> Cil_types.exp -> bool -> Dom.state Eval.or_bottom
          end
        type ('env, 'expr, 'v) evaluation_functions = {
          eval_and_warn : 'env -> 'expr -> 'v * bool * bool;
          env : Analysis.Dom.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 -> '-> Analysis.Val.t Gui_types.gui_res;
        }
        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 Bottom.or_bottom)
          evaluation_functions
        val lval_ev :
          (Analysis.Dom.t, Cil_types.lval, Analysis.Val.t Eval.flagged_value)
          evaluation_functions
        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 Bottom.or_bottom)
          evaluation_functions
        val predicate_ev :
          Gui_types.gui_loc ->
          (Eval_terms.eval_env, Cil_types.predicate,
           Eval_terms.predicate_status Bottom.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 Bottom.or_bottom)
          evaluation_functions
        val make_data_all_callstacks :
          ('a, 'b, 'c) evaluation_functions ->
          Gui_types.gui_loc ->
          '->
          (Gui_types.gui_callstack * Analysis.Val.t gui_selection_data) list *
          exn list
      end
end