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 :
                                                       'Abstract_domain.key ->
                                                       bool
                                                     val get :
                                                       'Abstract_domain.key ->
                                                       (state -> 'a) option
                                                     val set :
                                                       '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