sig   module type S =     sig       type state       type value       type origin       type loc       module Valuation :         sig           type t           type value = value           type origin = origin           type loc = loc           val empty : t           val find :             t -> Cil_types.exp -> (value, origin) Eval.record_val Eval.or_top           val add :             t -> Cil_types.exp -> (value, origin) Eval.record_val -> t           val fold :             (Cil_types.exp -> (value, origin) Eval.record_val -> '-> 'a) ->             t -> '-> 'a           val find_loc :             t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top           val remove : t -> Cil_types.exp -> t           val remove_loc : t -> Cil_types.lval -> t         end       val evaluate :         ?valuation:Evaluation.S.Valuation.t ->         ?reduction:bool ->         Evaluation.S.state ->         Cil_types.exp ->         (Evaluation.S.Valuation.t * Evaluation.S.value) Eval.evaluated       val copy_lvalue :         ?valuation:Evaluation.S.Valuation.t ->         Evaluation.S.state ->         Cil_types.lval ->         (Evaluation.S.Valuation.t * Evaluation.S.value Eval.flagged_value)         Eval.evaluated       val lvaluate :         ?valuation:Evaluation.S.Valuation.t ->         for_writing:bool ->         Evaluation.S.state ->         Cil_types.lval ->         (Evaluation.S.Valuation.t * Evaluation.S.loc * Cil_types.typ)         Eval.evaluated       val reduce :         ?valuation:Evaluation.S.Valuation.t ->         Evaluation.S.state ->         Cil_types.exp -> bool -> Evaluation.S.Valuation.t Eval.evaluated       val assume :         ?valuation:Evaluation.S.Valuation.t ->         Evaluation.S.state ->         Cil_types.exp ->         Evaluation.S.value -> Evaluation.S.Valuation.t Eval.or_bottom       val loc_size : Evaluation.S.loc -> Int_Base.t       val reinterpret :         Cil_types.exp ->         Cil_types.typ ->         Evaluation.S.value -> Evaluation.S.value Eval.evaluated       val do_promotion :         src_typ:Cil_types.typ ->         dst_typ:Cil_types.typ ->         Cil_types.exp ->         Evaluation.S.value -> Evaluation.S.value Eval.evaluated       val split_by_evaluation :         Cil_types.exp ->         Integer.t list ->         Evaluation.S.state list ->         (Integer.t * Evaluation.S.state list * bool) list *         Evaluation.S.state list       val check_copy_lval :         Cil_types.lval * Evaluation.S.loc ->         Cil_types.lval * Evaluation.S.loc -> bool Eval.evaluated       val check_non_overlapping :         Evaluation.S.state ->         Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated       val eval_function_exp :         Cil_types.exp ->         Evaluation.S.state ->         (Kernel_function.t * Evaluation.S.Valuation.t) list Eval.evaluated     end   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 Queries =     sig       type state       type value       type location       type origin       val extract_expr :         (Cil_types.exp -> value Eval.evaluated) ->         state -> Cil_types.exp -> (value * origin) Eval.evaluated       val extract_lval :         (Cil_types.exp -> value Eval.evaluated) ->         state ->         Cil_types.lval ->         Cil_types.typ -> location -> (value * origin) Eval.evaluated       val backward_location :         state ->         Cil_types.lval ->         Cil_types.typ ->         location -> value -> (location * value) Eval.or_bottom       val reduce_further :         state -> Cil_types.exp -> value -> (Cil_types.exp * value) list       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     end   module Make :     functor       (Value : Value) (Loc : sig                                type value = Value.t                                type location                                type offset                                val equal_loc : location -> location -> bool                                val equal_offset : offset -> offset -> bool                                val pretty_loc :                                  Format.formatter -> location -> unit                                val pretty_offset :                                  Format.formatter -> offset -> unit                                val to_value : location -> value                                val size : location -> Int_Base.t                                val partially_overlap :                                  location -> location -> bool                                val check_non_overlapping :                                  (Cil_types.lval * location) list ->                                  (Cil_types.lval * location) list ->                                  unit Eval.evaluated                                val offset_cardinal_zero_or_one :                                  offset -> bool                                val no_offset : offset                                val forward_field :                                  Cil_types.typ ->                                  Cil_types.fieldinfo -> offset -> offset                                val forward_index :                                  Cil_types.typ -> value -> offset -> offset                                val reduce_index_by_array_size :                                  size_expr:Cil_types.exp ->                                  index_expr:Cil_types.exp ->                                  Integer.t -> value -> value Eval.evaluated                                val forward_variable :                                  Cil_types.typ ->                                  Cil_types.varinfo ->                                  offset -> location Eval.or_bottom                                val forward_pointer :                                  Cil_types.typ ->                                  value -> offset -> location Eval.or_bottom                                val eval_varinfo :                                  Cil_types.varinfo -> location                                val reduce_loc_by_validity :                                  for_writing:bool ->                                  bitfield:bool ->                                  Cil_types.lval ->                                  location -> location Eval.evaluated                                val backward_variable :                                  Cil_types.varinfo ->                                  location -> offset Eval.or_bottom                                val backward_pointer :                                  value ->                                  offset ->                                  location -> (value * offset) Eval.or_bottom                                val backward_field :                                  Cil_types.typ ->                                  Cil_types.fieldinfo ->                                  offset -> offset Eval.or_bottom                                val backward_index :                                  Cil_types.typ ->                                  index:value ->                                  remaining:offset ->                                  offset -> (value * offset) Eval.or_bottom                              end) (Domain : sig                                               type state                                               type value = Value.t                                               type location = Loc.location                                               type origin                                               val extract_expr :                                                 (Cil_types.exp ->                                                  value Eval.evaluated) ->                                                 state ->                                                 Cil_types.exp ->                                                 (value * origin)                                                 Eval.evaluated                                               val extract_lval :                                                 (Cil_types.exp ->                                                  value Eval.evaluated) ->                                                 state ->                                                 Cil_types.lval ->                                                 Cil_types.typ ->                                                 location ->                                                 (value * origin)                                                 Eval.evaluated                                               val backward_location :                                                 state ->                                                 Cil_types.lval ->                                                 Cil_types.typ ->                                                 location ->                                                 value ->                                                 (location * value)                                                 Eval.or_bottom                                               val reduce_further :                                                 state ->                                                 Cil_types.exp ->                                                 value ->                                                 (Cil_types.exp * value) list                                               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                                             end->       sig         type state = Domain.state         type value = Value.t         type origin = Domain.origin         type loc = Loc.location         module Valuation :           sig             type t             type value = value             type origin = origin             type loc = loc             val empty : t             val find :               t ->               Cil_types.exp -> (value, origin) Eval.record_val Eval.or_top             val add :               t -> Cil_types.exp -> (value, origin) Eval.record_val -> t             val fold :               (Cil_types.exp -> (value, origin) Eval.record_val -> '-> 'a) ->               t -> '-> 'a             val find_loc :               t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top             val remove : t -> Cil_types.exp -> t             val remove_loc : t -> Cil_types.lval -> t           end         val evaluate :           ?valuation:Valuation.t ->           ?reduction:bool ->           state -> Cil_types.exp -> (Valuation.t * value) Eval.evaluated         val copy_lvalue :           ?valuation:Valuation.t ->           state ->           Cil_types.lval ->           (Valuation.t * value Eval.flagged_value) Eval.evaluated         val lvaluate :           ?valuation:Valuation.t ->           for_writing:bool ->           state ->           Cil_types.lval ->           (Valuation.t * loc * Cil_types.typ) Eval.evaluated         val reduce :           ?valuation:Valuation.t ->           state -> Cil_types.exp -> bool -> Valuation.t Eval.evaluated         val assume :           ?valuation:Valuation.t ->           state -> Cil_types.exp -> value -> Valuation.t Eval.or_bottom         val loc_size : loc -> Int_Base.t         val reinterpret :           Cil_types.exp -> Cil_types.typ -> value -> value Eval.evaluated         val do_promotion :           src_typ:Cil_types.typ ->           dst_typ:Cil_types.typ ->           Cil_types.exp -> value -> value Eval.evaluated         val split_by_evaluation :           Cil_types.exp ->           Integer.t list ->           state list -> (Integer.t * state list * bool) list * state list         val check_copy_lval :           Cil_types.lval * loc -> Cil_types.lval * loc -> bool Eval.evaluated         val check_non_overlapping :           state ->           Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated         val eval_function_exp :           Cil_types.exp ->           state -> (Kernel_function.t * Valuation.t) list Eval.evaluated       end end