sig   type config = {     cvalue : bool;     equalities : bool;     symbolic_locs : bool;     bitwise : bool;     gauges : bool;     apron_oct : bool;     apron_box : bool;     polka_loose : bool;     polka_strict : bool;     polka_equalities : bool;   }   val default_config : Abstractions.config   val legacy_config : Abstractions.config   val configure : unit -> Abstractions.config   module type Value =     sig       type 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       val top : t       val is_included : t -> t -> bool       val join : t -> t -> t       val narrow : t -> t -> t Eval.or_bottom       val zero : t       val float_zeros : t       val top_int : t       val inject_int : Cil_types.typ -> Integer.t -> t       val inject_address : Cil_types.varinfo -> t       val constant : Cil_types.exp -> Cil_types.constant -> t Eval.evaluated       val forward_unop :         context:Eval.unop_context ->         Cil_types.typ -> Cil_types.unop -> t -> t Eval.evaluated       val forward_binop :         context:Eval.binop_context ->         Cil_types.typ -> Cil_types.binop -> t -> t -> t Eval.evaluated       val backward_binop :         input_type:Cil_types.typ ->         resulting_type:Cil_types.typ ->         Cil_types.binop ->         left:t -> right:t -> result:t -> (t option * t option) Eval.or_bottom       val backward_unop :         typ_arg:Cil_types.typ ->         Cil_types.unop -> arg:t -> res:t -> t option Eval.or_bottom       val backward_cast :         src_typ:Cil_types.typ ->         dst_typ:Cil_types.typ ->         src_val:t -> dst_val:t -> t option Eval.or_bottom       val reinterpret :         Cil_types.exp -> Cil_types.typ -> t -> t Eval.evaluated       val do_promotion :         src_typ:Cil_types.typ ->         dst_typ:Cil_types.typ -> Cil_types.exp -> t -> t Eval.evaluated       val resolve_functions :         typ_pointer:Cil_types.typ ->         t -> Kernel_function.Hptset.t Eval.or_top * bool       val mem : 'Abstract_value.key -> bool       val get : 'Abstract_value.key -> (t -> 'a) option       val set : 'Abstract_value.key -> '-> t -> t       val reduce : t -> t     end   module type S =     sig       module Val : Value       module Loc :         sig           type value = Val.t           type location = Precise_locs.precise_location           type offset           val equal_loc : location -> location -> bool           val equal_offset : offset -> offset -> bool           val pretty_loc : Format.formatter -> location -> unit           val pretty_offset : Format.formatter -> offset -> unit           val to_value : location -> value           val size : location -> Int_Base.t           val partially_overlap : location -> location -> bool           val check_non_overlapping :             (Cil_types.lval * location) list ->             (Cil_types.lval * location) list -> unit Eval.evaluated           val offset_cardinal_zero_or_one : offset -> bool           val no_offset : offset           val forward_field :             Cil_types.typ -> Cil_types.fieldinfo -> offset -> offset           val forward_index : Cil_types.typ -> value -> offset -> offset           val reduce_index_by_array_size :             size_expr:Cil_types.exp ->             index_expr:Cil_types.exp ->             Integer.t -> value -> value Eval.evaluated           val forward_variable :             Cil_types.typ ->             Cil_types.varinfo -> offset -> location Eval.or_bottom           val forward_pointer :             Cil_types.typ -> value -> offset -> location Eval.or_bottom           val eval_varinfo : Cil_types.varinfo -> location           val reduce_loc_by_validity :             for_writing:bool ->             bitfield:bool ->             Cil_types.lval -> location -> location Eval.evaluated           val backward_variable :             Cil_types.varinfo -> location -> offset Eval.or_bottom           val backward_pointer :             value -> offset -> location -> (value * offset) Eval.or_bottom           val backward_field :             Cil_types.typ ->             Cil_types.fieldinfo -> offset -> offset Eval.or_bottom           val backward_index :             Cil_types.typ ->             index:value ->             remaining:offset -> offset -> (value * offset) Eval.or_bottom           val mem : 'Abstract_location.key -> bool           val get : 'Abstract_location.key -> (location -> 'a) option           val set : 'Abstract_location.key -> '-> location -> location         end       module Dom :         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 = Val.t           type location = Loc.location           type origin           val extract_expr :             (Cil_types.exp -> value Eval.evaluated) ->             t -> Cil_types.exp -> (value * origin) Eval.evaluated           val extract_lval :             (Cil_types.exp -> value Eval.evaluated) ->             t ->             Cil_types.lval ->             Cil_types.typ -> location -> (value * origin) Eval.evaluated           val backward_location :             t ->             Cil_types.lval ->             Cil_types.typ ->             location -> value -> (location * value) Eval.or_bottom           val reduce_further :             t -> Cil_types.exp -> value -> (Cil_types.exp * value) list           type return           module Return :             sig               type t = return               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 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 return = return                 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, return, value) Eval.call_action                 val finalize_call :                   Cil_types.stmt ->                   value Eval.call ->                   pre:state -> post:state -> state Eval.or_bottom                 val make_return :                   Cil_types.kernel_function ->                   Cil_types.stmt ->                   value Eval.assigned -> valuation -> state -> return                 val assign_return :                   Cil_types.stmt ->                   location Eval.left_value ->                   Cil_types.kernel_function ->                   return ->                   value Eval.assigned ->                   valuation -> state -> state Eval.or_bottom                 val default_call :                   Cil_types.stmt ->                   value Eval.call ->                   state -> (state, return, value) Eval.call_result                 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               end           val compute_using_specification :             Cil_types.kinstr ->             Cil_types.kernel_function * Cil_types.funspec ->             t -> (t, return, value) Eval.call_result           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 empty : unit -> t           val initialize_var :             t ->             Cil_types.lval -> location -> (value * bool) Eval.or_bottom -> t           val initialize_var_using_type : t -> Cil_types.varinfo -> t           val global_state : unit -> t Eval.or_bottom option           val filter_by_bases : Base.Hptset.t -> t -> t           val reuse : current_input:t -> previous_output:t -> t           val structure : t Abstract_domain.structure           module Store :             sig               val register_initial_state :                 Value_types.callstack -> state -> unit               val register_state_before_stmt :                 Value_types.callstack -> Cil_types.stmt -> state -> unit               val register_state_after_stmt :                 Value_types.callstack -> Cil_types.stmt -> state -> unit               val get_initial_state :                 Cil_types.kernel_function -> state Eval.or_bottom               val get_initial_state_by_callstack :                 Cil_types.kernel_function ->                 state Value_types.Callstack.Hashtbl.t option               val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom               val get_stmt_state_by_callstack :                 after:bool ->                 Cil_types.stmt ->                 state Value_types.Callstack.Hashtbl.t option             end           val mem : 'Abstract_domain.key -> bool           val get : 'Abstract_domain.key -> (state -> 'a) option           val set : 'Abstract_domain.key -> '-> state -> state         end     end   val make : Abstractions.config -> (module Abstractions.S)   module Legacy : S   module Default : S end