sig   module Make :     functor       (Value : Abstract_value.External) (Eva : sig                                                  type state                                                  type value = Value.t                                                  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: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->       sig         type state = Eva.state         type value = Value.t         type origin = Eva.origin         type loc = Eva.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: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