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