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_var :
        with_alarms:CilE.warn_mode ->
        Cil_types.stmt ->
        Cil_types.varinfo ->
        Cil_types.init ->
        Initialization.S.state ->
        Initialization.S.state Bottom.Type.or_bottom
    end
  module Make :
    functor
      (Value : Abstract_value.S) (Loc : sig
                                          type value = Value.t
                                          type location
                                          type offset
                                          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 partially_overlap :
                                            location -> location -> bool
                                          val check_non_overlapping :
                                            (Cil_types.lval * location) list ->
                                            (Cil_types.lval * location) list ->
                                            unit Eval.evaluated
                                          val offset_cardinal_zero_or_one :
                                            offset -> bool
                                          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 reduce_index_by_array_size :
                                            size_expr:Cil_types.exp ->
                                            index_expr:Cil_types.exp ->
                                            Integer.t ->
                                            value -> value Eval.evaluated
                                          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 reduce_loc_by_validity :
                                            for_writing:bool ->
                                            bitfield:bool ->
                                            Cil_types.lval ->
                                            location ->
                                            location Eval.evaluated
                                          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
                                        end) (Domain : sig
                                                         type 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
                                                             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 diff :
                                                               t -> t -> t
                                                             val subset :
                                                               t -> t -> bool
                                                             val iter :
                                                               (elt -> unit) ->
                                                               t -> unit
                                                             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 partition :
                                                               (elt -> bool) ->
                                                               t -> t * t
                                                             val cardinal :
                                                               t -> int
                                                             val elements :
                                                               t -> elt list
                                                             val choose :
                                                               t -> elt
                                                             val split :
                                                               elt ->
                                                               t ->
                                                               t * bool * t
                                                             val find :
                                                               elt ->
                                                               t -> elt
                                                             val of_list :
                                                               elt list -> t
                                                             val min_elt :
                                                               t -> elt
                                                             val max_elt :
                                                               t -> elt
                                                             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
                                                             val empty : 'a t
                                                             val is_empty :
                                                               'a t -> bool
                                                             val mem :
                                                               key ->
                                                               'a t -> bool
                                                             val add :
                                                               key ->
                                                               '->
                                                               '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 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 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 max_binding :
                                                               'a t ->
                                                               key * 'a
                                                             val choose :
                                                               'a t ->
                                                               key * 'a
                                                             val split :
                                                               key ->
                                                               'a t ->
                                                               'a t *
                                                               'a option *
                                                               'a t
                                                             val find :
                                                               key ->
                                                               'a t -> 'a
                                                             val map :
                                                               ('-> 'b) ->
                                                               'a t -> 'b t
                                                             val mapi :
                                                               (key ->
                                                                '-> 'b) ->
                                                               'a t -> 'b 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
                                                             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 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 structural_descr :
                                                               Structural_descr.t ->
                                                               Structural_descr.t
                                                             val make_type :
                                                               'Type.t ->
                                                               'a t Type.t
                                                             val memo :
                                                               'a t ->
                                                               key ->
                                                               (key -> 'a) ->
                                                               'a
                                                             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 join_and_is_included :
                                                           t -> t -> t * bool
                                                         val widen :
                                                           Cil_types.kernel_function ->
                                                           Cil_types.stmt ->
                                                           t -> t -> t
                                                         type value = Value.t
                                                         type location =
                                                             Loc.location
                                                         type origin
                                                         val extract_expr :
                                                           (Cil_types.exp ->
                                                            value
                                                            Eval.evaluated) ->
                                                           t ->
                                                           Cil_types.exp ->
                                                           (value * origin)
                                                           Eval.evaluated
                                                         val extract_lval :
                                                           (Cil_types.exp ->
                                                            value
                                                            Eval.evaluated) ->
                                                           t ->
                                                           Cil_types.lval ->
                                                           Cil_types.typ ->
                                                           location ->
                                                           (value * origin)
                                                           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
                                                         module Transfer :
                                                           functor
                                                             (Valuation : 
                                                             sig
                                                               type t
                                                               type value =
                                                                   value
                                                               type origin =
                                                                   origin
                                                               type loc =
                                                                   location
                                                               val find :
                                                                 t ->
                                                                 Cil_types.exp ->
                                                                 (value,
                                                                  origin)
                                                                 Eval.record_val
                                                                 Eval.or_top
                                                               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
                                                             end->
                                                             sig
                                                               type state = t
                                                               type value =
                                                                   value
                                                               type location =
                                                                   location
                                                               type valuation =
                                                                   Valuation.t
                                                               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
                                                             end
                                                         val compute_using_specification :
                                                           Cil_types.kinstr ->
                                                           value Eval.call ->
                                                           Cil_types.funspec ->
                                                           state ->
                                                           state list
                                                           Eval.or_bottom
                                                         type eval_env
                                                         val env_current_state :
                                                           eval_env ->
                                                           t Eval.or_bottom
                                                         val env_annot :
                                                           pre:t ->
                                                           here:t ->
                                                           unit -> eval_env
                                                         val env_pre_f :
                                                           pre:t ->
                                                           unit -> eval_env
                                                         val env_post_f :
                                                           pre:t ->
                                                           post:t ->
                                                           result:Cil_types.varinfo
                                                                  option ->
                                                           unit -> eval_env
                                                         val eval_predicate :
                                                           eval_env ->
                                                           Cil_types.predicate ->
                                                           Alarmset.status
                                                         val reduce_by_predicate :
                                                           eval_env ->
                                                           bool ->
                                                           Cil_types.predicate ->
                                                           eval_env
                                                         val enter_scope :
                                                           Cil_types.kernel_function ->
                                                           Cil_types.varinfo
                                                           list -> t -> t
                                                         val leave_scope :
                                                           Cil_types.kernel_function ->
                                                           Cil_types.varinfo
                                                           list -> 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 empty :
                                                           unit -> t
                                                         val initialize_var :
                                                           t ->
                                                           Cil_types.lval ->
                                                           location ->
                                                           (value * bool)
                                                           Eval.or_bottom ->
                                                           t
                                                         val initialize_var_using_type :
                                                           t ->
                                                           Cil_types.varinfo ->
                                                           t
                                                         val global_state :
                                                           unit ->
                                                           t Eval.or_bottom
                                                           option
                                                         val filter_by_bases :
                                                           Base.Hptset.t ->
                                                           t -> t
                                                         val reuse :
                                                           current_input:
                                                           t ->
                                                           previous_output:
                                                           t -> t
                                                         val structure :
                                                           t
                                                           Abstract_domain.structure
                                                         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
                                                         val mem :
                                                           'a
                                                           Abstract_domain.key ->
                                                           bool
                                                         val get :
                                                           'a
                                                           Abstract_domain.key ->
                                                           (state -> 'a)
                                                           option
                                                         val set :
                                                           'a
                                                           Abstract_domain.key ->
                                                           '->
                                                           state -> state
                                                       end) (Eva : sig
                                                                    type state =
                                                                    Domain.state
                                                                    type value =
                                                                    Domain.value
                                                                    type origin =
                                                                    Domain.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 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
        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_var :
          with_alarms:CilE.warn_mode ->
          Cil_types.stmt ->
          Cil_types.varinfo ->
          Cil_types.init -> Domain.t -> Domain.t Bottom.Type.or_bottom
      end
end