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 can_copy :
        ?valuation:Evaluation.S.Valuation.t ->
        is_ret:bool ->
        Evaluation.S.state ->
        Kernel_function.t ->
        Cil_types.lval ->
        Cil_types.exp ->
        (Cil_types.lval option * Evaluation.S.Valuation.t) 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 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 can_copy :
          ?valuation:Valuation.t ->
          is_ret:bool ->
          state ->
          Kernel_function.t ->
          Cil_types.lval ->
          Cil_types.exp ->
          (Cil_types.lval option * Valuation.t) 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 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