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 to_domain_valuation :
        Evaluation.S.Valuation.t ->
        (Evaluation.S.value, Evaluation.S.loc, Evaluation.S.origin)
        Abstract_domain.valuation
      val evaluate :
        ?valuation:Evaluation.S.Valuation.t ->
        ?reduction:bool ->
        ?subdivnb:int ->
        Evaluation.S.state ->
        Cil_types.exp ->
        (Evaluation.S.Valuation.t * Evaluation.S.value) Eval.evaluated
      val copy_lvalue :
        ?valuation:Evaluation.S.Valuation.t ->
        ?subdivnb:int ->
        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 ->
        ?subdivnb:int ->
        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 eval_function_exp :
        ?subdivnb:int ->
        Cil_types.exp ->
        ?args:Cil_types.exp list ->
        Evaluation.S.state ->
        (Kernel_function.t * Evaluation.S.Valuation.t) list Eval.evaluated
      val interpret_truth :
        alarm:(unit -> Alarms.t) ->
        '-> 'Abstract_value.truth -> '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 pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter
      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 one : t
      val top_int : t
      val inject_int : Cil_types.typ -> Integer.t -> t
      val assume_non_zero : t -> t Abstract_value.truth
      val assume_bounded :
        Abstract_value.bound_kind ->
        Abstract_value.bound -> t -> t Abstract_value.truth
      val assume_not_nan :
        assume_finite:bool -> Cil_types.fkind -> t -> t Abstract_value.truth
      val assume_pointer : t -> t Abstract_value.truth
      val assume_comparable :
        Abstract_value.pointer_comparison ->
        t -> t -> (t * t) Abstract_value.truth
      val constant : Cil_types.exp -> Cil_types.constant -> t
      val forward_unop :
        Cil_types.typ -> Cil_types.unop -> t -> t Eval.or_bottom
      val forward_binop :
        Cil_types.typ -> Cil_types.binop -> t -> t -> t Eval.or_bottom
      val rewrap_integer : Eval_typ.integer_range -> t -> t
      val forward_cast :
        src_type:Eval_typ.scalar_typ ->
        dst_type:Eval_typ.scalar_typ -> t -> t Eval.or_bottom
      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 resolve_functions : t -> Kernel_function.t list Eval.or_top * bool
      val replace_base : Base.substitution -> t -> t
      val structure : t Abstract.Value.structure
      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 :
        oracle:(Cil_types.exp -> value Eval.evaluated) ->
        Abstract_domain.evaluation_context ->
        state -> Cil_types.exp -> (value * origin option) Eval.evaluated
      val extract_lval :
        oracle:(Cil_types.exp -> value Eval.evaluated) ->
        Abstract_domain.evaluation_context ->
        state ->
        Cil_types.lval ->
        Cil_types.typ -> location -> (value * origin option) 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 top : location
               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 replace_base : Base.substitution -> location -> location
               val assume_no_overlap :
                 partial:bool ->
                 location ->
                 location -> (location * location) Abstract_location.truth
               val assume_valid_location :
                 for_writing:bool ->
                 bitfield:bool ->
                 location -> location Abstract_location.truth
               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 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 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 :
                    oracle:(Cil_types.exp -> value Eval.evaluated) ->
                    Abstract_domain.evaluation_context ->
                    state ->
                    Cil_types.exp -> (value * origin option) Eval.evaluated
                  val extract_lval :
                    oracle:(Cil_types.exp -> value Eval.evaluated) ->
                    Abstract_domain.evaluation_context ->
                    state ->
                    Cil_types.lval ->
                    Cil_types.typ ->
                    location -> (value * origin option) 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 to_domain_valuation :
          Valuation.t -> (value, loc, origin) Abstract_domain.valuation
        val evaluate :
          ?valuation:Valuation.t ->
          ?reduction:bool ->
          ?subdivnb:int ->
          state -> Cil_types.exp -> (Valuation.t * value) Eval.evaluated
        val copy_lvalue :
          ?valuation:Valuation.t ->
          ?subdivnb:int ->
          state ->
          Cil_types.lval ->
          (Valuation.t * value Eval.flagged_value) Eval.evaluated
        val lvaluate :
          ?valuation:Valuation.t ->
          ?subdivnb:int ->
          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 eval_function_exp :
          ?subdivnb:int ->
          Cil_types.exp ->
          ?args:Cil_types.exp list ->
          state -> (Kernel_function.t * Valuation.t) list Eval.evaluated
        val interpret_truth :
          alarm:(unit -> Alarms.t) ->
          '-> 'Abstract_value.truth -> 'Eval.evaluated
      end
end