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 disjoint : t -> t -> bool
                val diff : t -> t -> t
                val subset : t -> t -> bool
                val iter : (elt -> unit) -> t -> unit
                val map : (elt -> elt) -> t -> t
                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 filter_map : (elt -> elt option) -> t -> t
                val partition : (elt -> bool) -> t -> t * t
                val cardinal : t -> int
                val elements : t -> elt list
                val min_elt : t -> elt
                val min_elt_opt : t -> elt option
                val max_elt : t -> elt
                val max_elt_opt : t -> elt option
                val choose : t -> elt
                val choose_opt : t -> elt option
                val split : elt -> t -> t * bool * t
                val find : elt -> t -> elt
                val find_opt : elt -> t -> elt option
                val find_first : (elt -> bool) -> t -> elt
                val find_first_opt : (elt -> bool) -> t -> elt option
                val find_last : (elt -> bool) -> t -> elt
                val find_last_opt : (elt -> bool) -> t -> elt option
                val of_list : elt list -> t
                val to_seq_from : elt -> t -> elt Seq.t
                val to_seq : t -> elt Seq.t
                val add_seq : elt Seq.t -> t -> t
                val of_seq : elt Seq.t -> t
                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 update : key -> ('a option -> 'a option) -> '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 union :
                  (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a 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 filter_map : (key -> '-> 'b option) -> 'a t -> 'b 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 min_binding_opt : 'a t -> (key * 'a) option
                val max_binding : 'a t -> key * 'a
                val max_binding_opt : 'a t -> (key * 'a) option
                val choose : 'a t -> key * 'a
                val choose_opt : 'a t -> (key * 'a) option
                val split : key -> 'a t -> 'a t * 'a option * 'a t
                val find : key -> 'a t -> 'a
                val find_opt : key -> 'a t -> 'a option
                val find_first : (key -> bool) -> 'a t -> key * 'a
                val find_first_opt :
                  (key -> bool) -> 'a t -> (key * 'a) option
                val find_last : (key -> bool) -> 'a t -> key * 'a
                val find_last_opt :
                  (key -> bool) -> 'a t -> (key * 'a) option
                val map : ('-> 'b) -> 'a t -> 'b t
                val mapi : (key -> '-> 'b) -> 'a t -> 'b t
                val to_seq : 'a t -> (key * 'a) Seq.t
                val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
                val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
                val of_seq : (key * 'a) Seq.t -> 'a 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 to_seq : 'a t -> (key * 'a) Seq.t
                val to_seq_keys : 'a t -> key Seq.t
                val to_seq_values : 'a t -> 'Seq.t
                val add_seq : 'a t -> (key * 'a) Seq.t -> unit
                val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
                val of_seq : (key * 'a) Seq.t -> 'a t
                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 find_opt : 'a t -> key -> 'a option
                val find_def : 'a t -> key -> '-> 'a
                val memo : 'a t -> key -> (key -> 'a) -> 'a
                val structural_descr :
                  Structural_descr.t -> Structural_descr.t
                val make_type : 'Type.t -> 'a t Type.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
            val top : t
            val is_included : t -> t -> bool
            val join : t -> t -> t
            val widen :
              Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
            val narrow : t -> t -> t Eval.or_bottom
            type value = Value.t
            type location
            type origin
            val extract_expr :
              oracle:(Cil_types.exp -> value Eval.evaluated) ->
              Abstract_domain.evaluation_context ->
              t -> Cil_types.exp -> (value * origin option) Eval.evaluated
            val extract_lval :
              oracle:(Cil_types.exp -> value Eval.evaluated) ->
              Abstract_domain.evaluation_context ->
              t ->
              Cil_types.lval ->
              Cil_types.typ ->
              location -> (value * origin option) 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
            val update :
              (value, location, origin) Abstract_domain.valuation ->
              t -> t Eval.or_bottom
            val assign :
              Cil_types.kinstr ->
              location Eval.left_value ->
              Cil_types.exp ->
              (location, value) Eval.assigned ->
              (value, location, origin) Abstract_domain.valuation ->
              t -> t Eval.or_bottom
            val assume :
              Cil_types.stmt ->
              Cil_types.exp ->
              bool ->
              (value, location, origin) Abstract_domain.valuation ->
              t -> t Eval.or_bottom
            val start_call :
              Cil_types.stmt ->
              (location, value) Eval.call ->
              Eval.recursion option ->
              (value, location, origin) Abstract_domain.valuation ->
              t -> t Eval.or_bottom
            val finalize_call :
              Cil_types.stmt ->
              (location, value) Eval.call ->
              Eval.recursion option -> pre:t -> post:t -> t Eval.or_bottom
            val show_expr :
              (value, location, origin) Abstract_domain.valuation ->
              t -> Format.formatter -> Cil_types.exp -> unit
            val logic_assign :
              (location Eval.logic_assign * state) option ->
              location -> state -> state
            val evaluate_predicate :
              state Abstract_domain.logic_environment ->
              state -> Cil_types.predicate -> Alarmset.status
            val reduce_by_predicate :
              state Abstract_domain.logic_environment ->
              state -> Cil_types.predicate -> bool -> state Eval.or_bottom
            val enter_scope :
              Abstract_domain.variable_kind ->
              Cil_types.varinfo list -> t -> t
            val leave_scope :
              Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
            val empty : unit -> t
            val initialize_variable :
              Cil_types.lval ->
              location ->
              initialized:bool -> Abstract_domain.init_value -> t -> t
            val initialize_variable_using_type :
              Abstract_domain.variable_kind -> Cil_types.varinfo -> 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 relate :
              Cil_types.kernel_function ->
              Base.Hptset.t -> t -> Base.SetLattice.t
            val filter :
              Cil_types.kernel_function ->
              [ `Post | `Pre ] -> Base.Hptset.t -> t -> t
            val reuse :
              Cil_types.kernel_function ->
              Base.Hptset.t -> current_input:t -> previous_output:t -> t
            val log_category : Value_parameters.category
            module Store :
              sig
                val register_global_state : state Eval.or_bottom -> unit
                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_global_state : unit -> state Eval.or_bottom
                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 Eval.or_top_or_bottom
                val get_stmt_state :
                  after:bool -> Cil_types.stmt -> state Eval.or_bottom
                val get_stmt_state_by_callstack :
                  after:bool ->
                  Cil_types.stmt ->
                  state Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom
              end
            val post_analysis : t Eval.or_bottom -> unit
            val structure : t Abstract.Domain.structure
          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 disjoint : t -> t -> bool
                 val diff : t -> t -> t
                 val subset : t -> t -> bool
                 val iter : (elt -> unit) -> t -> unit
                 val map : (elt -> elt) -> t -> t
                 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 filter_map : (elt -> elt option) -> t -> t
                 val partition : (elt -> bool) -> t -> t * t
                 val cardinal : t -> int
                 val elements : t -> elt list
                 val min_elt : t -> elt
                 val min_elt_opt : t -> elt option
                 val max_elt : t -> elt
                 val max_elt_opt : t -> elt option
                 val choose : t -> elt
                 val choose_opt : t -> elt option
                 val split : elt -> t -> t * bool * t
                 val find : elt -> t -> elt
                 val find_opt : elt -> t -> elt option
                 val find_first : (elt -> bool) -> t -> elt
                 val find_first_opt : (elt -> bool) -> t -> elt option
                 val find_last : (elt -> bool) -> t -> elt
                 val find_last_opt : (elt -> bool) -> t -> elt option
                 val of_list : elt list -> t
                 val to_seq_from : elt -> t -> elt Seq.t
                 val to_seq : t -> elt Seq.t
                 val add_seq : elt Seq.t -> t -> t
                 val of_seq : elt Seq.t -> t
                 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 update : key -> ('a option -> 'a option) -> '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 union :
                   (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a 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 filter_map : (key -> '-> 'b option) -> 'a t -> 'b 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 min_binding_opt : 'a t -> (key * 'a) option
                 val max_binding : 'a t -> key * 'a
                 val max_binding_opt : 'a t -> (key * 'a) option
                 val choose : 'a t -> key * 'a
                 val choose_opt : 'a t -> (key * 'a) option
                 val split : key -> 'a t -> 'a t * 'a option * 'a t
                 val find : key -> 'a t -> 'a
                 val find_opt : key -> 'a t -> 'a option
                 val find_first : (key -> bool) -> 'a t -> key * 'a
                 val find_first_opt :
                   (key -> bool) -> 'a t -> (key * 'a) option
                 val find_last : (key -> bool) -> 'a t -> key * 'a
                 val find_last_opt :
                   (key -> bool) -> 'a t -> (key * 'a) option
                 val map : ('-> 'b) -> 'a t -> 'b t
                 val mapi : (key -> '-> 'b) -> 'a t -> 'b t
                 val to_seq : 'a t -> (key * 'a) Seq.t
                 val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
                 val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
                 val of_seq : (key * 'a) Seq.t -> 'a 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 to_seq : 'a t -> (key * 'a) Seq.t
                 val to_seq_keys : 'a t -> key Seq.t
                 val to_seq_values : 'a t -> 'Seq.t
                 val add_seq : 'a t -> (key * 'a) Seq.t -> unit
                 val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
                 val of_seq : (key * 'a) Seq.t -> 'a t
                 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 find_opt : 'a t -> key -> 'a option
                 val find_def : 'a t -> key -> '-> 'a
                 val memo : 'a t -> key -> (key -> 'a) -> 'a
                 val structural_descr :
                   Structural_descr.t -> Structural_descr.t
                 val make_type : 'Type.t -> 'a t Type.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
             val top : t
             val is_included : t -> t -> bool
             val join : t -> t -> t
             val widen :
               Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
             val narrow : t -> t -> t Eval.or_bottom
             type value = Left.value
             type location = Left.location
             type origin
             val extract_expr :
               oracle:(Cil_types.exp -> value Eval.evaluated) ->
               Abstract_domain.evaluation_context ->
               t -> Cil_types.exp -> (value * origin option) Eval.evaluated
             val extract_lval :
               oracle:(Cil_types.exp -> value Eval.evaluated) ->
               Abstract_domain.evaluation_context ->
               t ->
               Cil_types.lval ->
               Cil_types.typ ->
               location -> (value * origin option) 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
             val update :
               (value, location, origin) Abstract_domain.valuation ->
               t -> t Eval.or_bottom
             val assign :
               Cil_types.kinstr ->
               location Eval.left_value ->
               Cil_types.exp ->
               (location, value) Eval.assigned ->
               (value, location, origin) Abstract_domain.valuation ->
               t -> t Eval.or_bottom
             val assume :
               Cil_types.stmt ->
               Cil_types.exp ->
               bool ->
               (value, location, origin) Abstract_domain.valuation ->
               t -> t Eval.or_bottom
             val start_call :
               Cil_types.stmt ->
               (location, value) Eval.call ->
               Eval.recursion option ->
               (value, location, origin) Abstract_domain.valuation ->
               t -> t Eval.or_bottom
             val finalize_call :
               Cil_types.stmt ->
               (location, value) Eval.call ->
               Eval.recursion option -> pre:t -> post:t -> t Eval.or_bottom
             val show_expr :
               (value, location, origin) Abstract_domain.valuation ->
               t -> Format.formatter -> Cil_types.exp -> unit
             val logic_assign :
               (location Eval.logic_assign * state) option ->
               location -> state -> state
             val evaluate_predicate :
               state Abstract_domain.logic_environment ->
               state -> Cil_types.predicate -> Alarmset.status
             val reduce_by_predicate :
               state Abstract_domain.logic_environment ->
               state -> Cil_types.predicate -> bool -> state Eval.or_bottom
             val enter_scope :
               Abstract_domain.variable_kind ->
               Cil_types.varinfo list -> t -> t
             val leave_scope :
               Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
             val empty : unit -> t
             val initialize_variable :
               Cil_types.lval ->
               location ->
               initialized:bool -> Abstract_domain.init_value -> t -> t
             val initialize_variable_using_type :
               Abstract_domain.variable_kind -> Cil_types.varinfo -> 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 relate :
               Cil_types.kernel_function ->
               Base.Hptset.t -> t -> Base.SetLattice.t
             val filter :
               Cil_types.kernel_function ->
               [ `Post | `Pre ] -> Base.Hptset.t -> t -> t
             val reuse :
               Cil_types.kernel_function ->
               Base.Hptset.t -> current_input:t -> previous_output:t -> t
             val log_category : Value_parameters.category
             module Store :
               sig
                 val register_global_state : state Eval.or_bottom -> unit
                 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_global_state : unit -> state Eval.or_bottom
                 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
                   Eval.or_top_or_bottom
                 val get_stmt_state :
                   after:bool -> Cil_types.stmt -> state Eval.or_bottom
                 val get_stmt_state_by_callstack :
                   after:bool ->
                   Cil_types.stmt ->
                   state Value_types.Callstack.Hashtbl.t
                   Eval.or_top_or_bottom
               end
             val post_analysis : t Eval.or_bottom -> unit
             val structure : t Abstract.Domain.structure
           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 disjoint : t -> t -> bool
        val diff : t -> t -> t
        val subset : t -> t -> bool
        val iter : (elt -> unit) -> t -> unit
        val map : (elt -> elt) -> t -> t
        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 filter_map : (elt -> elt option) -> t -> t
        val partition : (elt -> bool) -> t -> t * t
        val cardinal : t -> int
        val elements : t -> elt list
        val min_elt : t -> elt
        val min_elt_opt : t -> elt option
        val max_elt : t -> elt
        val max_elt_opt : t -> elt option
        val choose : t -> elt
        val choose_opt : t -> elt option
        val split : elt -> t -> t * bool * t
        val find : elt -> t -> elt
        val find_opt : elt -> t -> elt option
        val find_first : (elt -> bool) -> t -> elt
        val find_first_opt : (elt -> bool) -> t -> elt option
        val find_last : (elt -> bool) -> t -> elt
        val find_last_opt : (elt -> bool) -> t -> elt option
        val of_list : elt list -> t
        val to_seq_from : elt -> t -> elt Seq.t
        val to_seq : t -> elt Seq.t
        val add_seq : elt Seq.t -> t -> t
        val of_seq : elt Seq.t -> t
        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 update : key -> ('a option -> 'a option) -> '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 union : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a 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 filter_map : (key -> '-> 'b option) -> 'a t -> 'b 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 min_binding_opt : 'a t -> (key * 'a) option
        val max_binding : 'a t -> key * 'a
        val max_binding_opt : 'a t -> (key * 'a) option
        val choose : 'a t -> key * 'a
        val choose_opt : 'a t -> (key * 'a) option
        val split : key -> 'a t -> 'a t * 'a option * 'a t
        val find : key -> 'a t -> 'a
        val find_opt : key -> 'a t -> 'a option
        val find_first : (key -> bool) -> 'a t -> key * 'a
        val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
        val find_last : (key -> bool) -> 'a t -> key * 'a
        val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
        val map : ('-> 'b) -> 'a t -> 'b t
        val mapi : (key -> '-> 'b) -> 'a t -> 'b t
        val to_seq : 'a t -> (key * 'a) Seq.t
        val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
        val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
        val of_seq : (key * 'a) Seq.t -> 'a 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 to_seq : 'a t -> (key * 'a) Seq.t
        val to_seq_keys : 'a t -> key Seq.t
        val to_seq_values : 'a t -> 'Seq.t
        val add_seq : 'a t -> (key * 'a) Seq.t -> unit
        val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
        val of_seq : (key * 'a) Seq.t -> 'a t
        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 find_opt : 'a t -> key -> 'a option
        val find_def : 'a t -> key -> '-> 'a
        val memo : 'a t -> key -> (key -> 'a) -> 'a
        val structural_descr : Structural_descr.t -> Structural_descr.t
        val make_type : 'Type.t -> 'a t Type.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
    val top : t
    val is_included : t -> t -> bool
    val join : t -> t -> t
    val widen : Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
    val narrow : t -> t -> t Eval.or_bottom
    type value = Value.t
    type location = Left.location
    type origin
    val extract_expr :
      oracle:(Cil_types.exp -> value Eval.evaluated) ->
      Abstract_domain.evaluation_context ->
      t -> Cil_types.exp -> (value * origin option) Eval.evaluated
    val extract_lval :
      oracle:(Cil_types.exp -> value Eval.evaluated) ->
      Abstract_domain.evaluation_context ->
      t ->
      Cil_types.lval ->
      Cil_types.typ -> location -> (value * origin option) 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
    val update :
      (value, location, origin) Abstract_domain.valuation ->
      t -> t Eval.or_bottom
    val assign :
      Cil_types.kinstr ->
      location Eval.left_value ->
      Cil_types.exp ->
      (location, value) Eval.assigned ->
      (value, location, origin) Abstract_domain.valuation ->
      t -> t Eval.or_bottom
    val assume :
      Cil_types.stmt ->
      Cil_types.exp ->
      bool ->
      (value, location, origin) Abstract_domain.valuation ->
      t -> t Eval.or_bottom
    val start_call :
      Cil_types.stmt ->
      (location, value) Eval.call ->
      Eval.recursion option ->
      (value, location, origin) Abstract_domain.valuation ->
      t -> t Eval.or_bottom
    val finalize_call :
      Cil_types.stmt ->
      (location, value) Eval.call ->
      Eval.recursion option -> pre:t -> post:t -> t Eval.or_bottom
    val show_expr :
      (value, location, origin) Abstract_domain.valuation ->
      t -> Format.formatter -> Cil_types.exp -> unit
    val logic_assign :
      (location Eval.logic_assign * state) option ->
      location -> state -> state
    val evaluate_predicate :
      state Abstract_domain.logic_environment ->
      state -> Cil_types.predicate -> Alarmset.status
    val reduce_by_predicate :
      state Abstract_domain.logic_environment ->
      state -> Cil_types.predicate -> bool -> state Eval.or_bottom
    val enter_scope :
      Abstract_domain.variable_kind -> Cil_types.varinfo list -> t -> t
    val leave_scope :
      Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
    val empty : unit -> t
    val initialize_variable :
      Cil_types.lval ->
      location -> initialized:bool -> Abstract_domain.init_value -> t -> t
    val initialize_variable_using_type :
      Abstract_domain.variable_kind -> Cil_types.varinfo -> 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 relate :
      Cil_types.kernel_function -> Base.Hptset.t -> t -> Base.SetLattice.t
    val filter :
      Cil_types.kernel_function ->
      [ `Post | `Pre ] -> Base.Hptset.t -> t -> t
    val reuse :
      Cil_types.kernel_function ->
      Base.Hptset.t -> current_input:t -> previous_output:t -> t
    val log_category : Value_parameters.category
    module Store :
      sig
        val register_global_state : state Eval.or_bottom -> unit
        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_global_state : unit -> state Eval.or_bottom
        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 Eval.or_top_or_bottom
        val get_stmt_state :
          after:bool -> Cil_types.stmt -> state Eval.or_bottom
        val get_stmt_state_by_callstack :
          after:bool ->
          Cil_types.stmt ->
          state Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom
      end
    val post_analysis : t Eval.or_bottom -> unit
    val structure : t Abstract.Domain.structure
  end