functor
  (Value : Abstract_value.S) (Location : Abstract_location.External) (Domain : 
  sig
    type state
    type value = Value.t
    type location = Location.location
    type valuation
    val update : valuation -> state -> state
    val assign :
      Cil_types.kinstr ->
      location Eval.left_value ->
      Cil_types.exp ->
      value Eval.assigned -> valuation -> state -> state Eval.or_bottom
    val assume :
      Cil_types.stmt ->
      Cil_types.exp -> bool -> valuation -> state -> state Eval.or_bottom
    val start_call :
      Cil_types.stmt ->
      value Eval.call -> valuation -> state -> state Eval.call_action
    val finalize_call :
      Cil_types.stmt ->
      value Eval.call -> pre:state -> post:state -> state Eval.or_bottom
    val approximate_call :
      Cil_types.stmt -> value Eval.call -> state -> state list Eval.or_bottom
    val leave_scope :
      Cil_types.kernel_function -> Cil_types.varinfo list -> state -> state
    module Store :
      sig
        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_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 option
        val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom
        val get_stmt_state_by_callstack :
          after:bool ->
          Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option
      end
    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
  end) (Init : sig
                 val initial_state :
                   lib_entry:bool -> Domain.state Bottom.Type.or_bottom
                 val initial_state_with_formals :
                   lib_entry:bool ->
                   Cil_types.kernel_function ->
                   Domain.state Bottom.Type.or_bottom
                 val initialize_var :
                   with_alarms:CilE.warn_mode ->
                   Cil_types.stmt ->
                   Cil_types.varinfo ->
                   Cil_types.init ->
                   Domain.state -> Domain.state Bottom.Type.or_bottom
               end) (Eva : sig
                             type state = Domain.state
                             type value = Domain.value
                             type origin
                             type loc = Domain.location
                             module Valuation :
                               sig
                                 type t = Domain.valuation
                                 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 evaluate :
                               ?valuation:Valuation.t ->
                               ?reduction:bool ->
                               state ->
                               Cil_types.exp ->
                               (Valuation.t * value) Eval.evaluated
                             val copy_lvalue :
                               ?valuation:Valuation.t ->
                               state ->
                               Cil_types.lval ->
                               (Valuation.t * value Eval.flagged_value)
                               Eval.evaluated
                             val lvaluate :
                               ?valuation:Valuation.t ->
                               for_writing:bool ->
                               state ->
                               Cil_types.lval ->
                               (Valuation.t * loc * Cil_types.typ)
                               Eval.evaluated
                             val can_copy :
                               ?valuation:Valuation.t ->
                               is_ret:bool ->
                               state ->
                               Kernel_function.t ->
                               Cil_types.lval ->
                               Cil_types.exp ->
                               (Cil_types.lval option * Valuation.t)
                               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 split_by_evaluation :
                               Cil_types.exp ->
                               Integer.t list ->
                               state list ->
                               (Integer.t * state list * bool) list *
                               state list
                             val check_copy_lval :
                               Cil_types.lval * loc ->
                               Cil_types.lval * loc -> bool Eval.evaluated
                             val check_non_overlapping :
                               state ->
                               Cil_types.lval list ->
                               Cil_types.lval list -> unit Eval.evaluated
                             val eval_function_exp :
                               Cil_types.exp ->
                               state ->
                               (Kernel_function.t * Valuation.t) list
                               Eval.evaluated
                           end->
  sig
    type state = Domain.state
    type value = Domain.value
    val init :
      with_alarms:CilE.warn_mode ->
      state ->
      Cil_types.kernel_function ->
      Cil_types.stmt ->
      Cil_types.varinfo -> Cil_types.init -> state Eval.or_bottom
    val assign :
      with_alarms:CilE.warn_mode ->
      state ->
      Cil_types.kernel_function ->
      Cil_types.stmt ->
      Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
    val assume :
      with_alarms:CilE.warn_mode ->
      state ->
      Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
    val call :
      with_alarms:CilE.warn_mode ->
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil_types.exp ->
      Cil_types.exp list ->
      state -> state list Eval.or_bottom * Value_types.cacheable
    val split_final_states :
      Cil_types.kernel_function ->
      Cil_types.exp -> Integer.t list -> state list -> state list list
    val check_unspecified_sequence :
      with_alarms:CilE.warn_mode ->
      Cil_types.stmt ->
      state ->
      (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
       Cil_types.lval list * Cil_types.stmt ref list)
      list -> unit Eval.or_bottom
    type call_result = {
      states : state list Eval.or_bottom;
      cacheable : Value_types.cacheable;
    }
    val compute_call_ref :
      (Cil_types.kinstr -> value Eval.call -> state -> call_result) ref
  end