functor   (Value : Abstract_value.S) (Location : Abstract_location.External) (Domain :    sig     type state     type return     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, return, value) Eval.call_action     val finalize_call :       Cil_types.stmt ->       value Eval.call -> pre:state -> post:state -> state Eval.or_bottom     val make_return :       Cil_types.kernel_function ->       Cil_types.stmt -> value Eval.assigned -> valuation -> state -> return     val assign_return :       Cil_types.stmt ->       location Eval.left_value ->       Cil_types.kernel_function ->       return ->       value Eval.assigned -> valuation -> state -> state Eval.or_bottom     val default_call :       Cil_types.stmt ->       value Eval.call -> state -> (state, return, value) Eval.call_result     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 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) (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 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 loc_size : loc -> Int_Base.t                 val reinterpret :                   Cil_types.exp ->                   Cil_types.typ -> value -> value Eval.evaluated                 val do_promotion :                   src_typ:Cil_types.typ ->                   dst_typ:Cil_types.typ ->                   Cil_types.exp -> value -> value Eval.evaluated                 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     type return = Domain.return     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 return :       with_alarms:CilE.warn_mode ->       Cil_types.kernel_function ->       Cil_types.stmt ->       Cil_types.lval option ->       state -> (state, return, value) Eval.return_state Eval.or_bottom     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 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 ->       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 res =         (state, return, value) Eval.call_result * Value_types.cacheable     val compute_call_ref :       (Cil_types.kinstr -> value Eval.call -> state -> res) ref   end