sig
  module type S =
    sig
      type state
      val initial_state :
        lib_entry:bool -> Initialization.S.state Bottom.Type.or_bottom
      val initial_state_with_formals :
        lib_entry:bool ->
        Cil_types.kernel_function ->
        Initialization.S.state Bottom.Type.or_bottom
      val initialize_local_variable :
        Cil_types.stmt ->
        Cil_types.varinfo ->
        Cil_types.init ->
        Initialization.S.state ->
        Initialization.S.state Bottom.Type.or_bottom
    end
  module Make :
    functor
      (Domain : Abstract.Domain.External) (Eva : sig
                                                   type state = Domain.state
                                                   type value
                                                   type origin
                                                   type loc = Domain.location
                                                   module Valuation :
                                                     sig
                                                       type 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) (Transfer : sig
                                                                    type state =
                                                                    Domain.t
                                                                    type value
                                                                    type location
                                                                    val assign :
                                                                    state ->
                                                                    Cil_types.kinstr ->
                                                                    Cil_types.lval ->
                                                                    Cil_types.exp ->
                                                                    state
                                                                    Eval.or_bottom
                                                                    val assume :
                                                                    state ->
                                                                    Cil_types.stmt ->
                                                                    Cil_types.exp ->
                                                                    bool ->
                                                                    state
                                                                    Eval.or_bottom
                                                                    val call :
                                                                    Cil_types.stmt ->
                                                                    Cil_types.lval
                                                                    option ->
                                                                    Cil_types.exp ->
                                                                    Cil_types.exp
                                                                    list ->
                                                                    state ->
                                                                    state
                                                                    list
                                                                    Eval.or_bottom *
                                                                    Value_types.cacheable
                                                                    val check_unspecified_sequence :
                                                                    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
                                                                    val enter_scope :
                                                                    Cil_types.kernel_function ->
                                                                    Cil_types.varinfo
                                                                    list ->
                                                                    state ->
                                                                    state
                                                                    type call_result = {
                                                                    states :
                                                                    state
                                                                    list
                                                                    Eval.or_bottom;
                                                                    cacheable :
                                                                    Value_types.cacheable;
                                                                    builtin :
                                                                    bool;
                                                                    }
                                                                    val compute_call_ref :
                                                                    (Cil_types.stmt ->
                                                                    (location,
                                                                    value)
                                                                    Eval.call ->
                                                                    state ->
                                                                    call_result)
                                                                    ref
                                                                  end->
      sig
        val initial_state : lib_entry:bool -> Domain.t Bottom.Type.or_bottom
        val initial_state_with_formals :
          lib_entry:bool ->
          Cil_types.kernel_function -> Domain.t Bottom.Type.or_bottom
        val initialize_local_variable :
          Cil_types.stmt ->
          Cil_types.varinfo ->
          Cil_types.init -> Domain.t -> Domain.t Bottom.Type.or_bottom
      end
end