sig
  module Make :
    functor
      (Value : Abstract_value.S) (Left : 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
                                           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
                                         end) (Right : 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 =
                                                             Left.value
                                                         type location =
                                                             Left.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
                                                       end->
      sig
        type state = Left.state * Right.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 = Left.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
      end
end