sig
  type 'a or_bottom = [ `Bottom | `Value of 'a ]
  type 'a or_top = [ `Top | `Value of 'a ]
  type 'a or_top_bottom = [ `Bottom | `Top | `Value of 'a ]
  module Bottom :
    sig
      type 'a t = 'a or_bottom
      module Operators :
        sig
          val ( >>- ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( >>-: ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( let+ ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
          val ( let* ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
        end
      module Make_Datatype :
        functor (Domain : Datatype.S->
          sig
            type t = Domain.t or_bottom
            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 Bound_Lattice :
        functor (Lattice : Lattice_type.Join_Semi_Lattice->
          sig
            type t = Lattice.t or_bottom
            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 join : t -> t -> t
            val is_included : t -> t -> bool
            val bottom : t
          end
      val is_bottom : 'a t -> bool
      val non_bottom : 'a t -> 'a
      val value : bottom:'-> 'a t -> 'a
      val hash : ('-> int) -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val pretty_bottom : Format.formatter -> unit
      val pretty :
        (Format.formatter -> '-> unit) -> Format.formatter -> 'a t -> unit
      val is_included : ('-> '-> bool) -> 'a t -> 'b t -> bool
      val join : ('-> '-> 'a) -> 'a t -> 'a t -> 'a t
      val join_list : ('-> '-> 'a) -> 'a t list -> 'a t
      val narrow : ('-> '-> 'a t) -> 'a t -> 'a t -> 'a t
      val iter : ('-> unit) -> 'a t -> unit
      val fold : bottom:'-> ('-> 'b) -> 'a t -> 'b
      val map : ('-> 'b) -> 'a t -> 'b t
      val zip : 'a t -> 'b t -> ('a * 'b) t
      val to_option : 'a t -> 'a option
      val of_option : 'a option -> 'a t
      val to_list : 'a t -> 'a list
      val bot_of_list : 'a list -> 'a list t
      val list_of_bot : 'a list t -> 'a list
      val list_values : 'a t list -> 'a list
      val add_to_list : 'a t -> 'a list -> 'a list
    end
  module Top :
    sig
      type 'a t = 'a or_top
      module Operators :
        sig
          val ( >>- ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( >>-: ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( let+ ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
          val ( let* ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
        end
      val is_top : 'a t -> bool
      val non_top : 'a t -> 'a
      val value : top:'-> 'a t -> 'a
      val hash : ('-> int) -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val pretty_top : Format.formatter -> unit
      val pretty :
        (Format.formatter -> '-> unit) -> Format.formatter -> 'a t -> unit
      val join : ('-> '-> 'a t) -> 'a t -> 'a t -> 'a t
      val narrow : ('-> '-> 'a) -> 'a t -> 'a t -> 'a t
      val zip : 'a t -> 'b t -> ('a * 'b) t
      val to_option : 'a t -> 'a option
      val of_option : 'a option -> 'a t
    end
  module TopBottom :
    sig
      type 'a t = 'a or_top_bottom
      module Operators :
        sig
          val ( >>- ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( >>-: ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( let+ ) : [< 'a t ] -> ('-> 'b) -> [> 'b t ]
          val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
          val ( let* ) : [< 'a t ] -> ('-> ([> 'b t ] as 'c)) -> 'c
          val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
        end
      val hash : ('-> int) -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val pretty :
        (Format.formatter -> '-> unit) -> Format.formatter -> 'a t -> unit
      val join : ('-> '-> [< 'a t ]) -> 'a t -> 'a t -> 'a t
      val narrow : ('-> '-> [< 'a t ]) -> 'a t -> 'a t -> 'a t
    end
  val ( >>- ) : [< 'Bottom.t ] -> ('-> ([> 'Bottom.t ] as 'c)) -> 'c
  val ( >>-: ) : [< 'Bottom.t ] -> ('-> 'b) -> [> 'Bottom.t ]
  val ( let+ ) : [< 'Bottom.t ] -> ('-> 'b) -> [> 'Bottom.t ]
  val ( and+ ) :
    [< 'Bottom.t ] -> [< 'Bottom.t ] -> [> ('a * 'b) Bottom.t ]
  val ( let* ) : [< 'Bottom.t ] -> ('-> ([> 'Bottom.t ] as 'c)) -> 'c
  val ( and* ) :
    [< 'Bottom.t ] -> [< 'Bottom.t ] -> [> ('a * 'b) Bottom.t ]
  type 't with_alarms = 't * Alarmset.t
  type 't evaluated = 't or_bottom Eval.with_alarms
  val ( >>= ) :
    'Eval.evaluated -> ('-> 'Eval.evaluated) -> 'Eval.evaluated
  val ( >>=. ) :
    'Eval.evaluated -> ('-> 'b or_bottom) -> 'Eval.evaluated
  val ( >>=: ) : 'Eval.evaluated -> ('-> 'b) -> 'Eval.evaluated
  type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ]
  type reductness = Unreduced | Reduced | Created | Dull
  type 'a flagged_value = {
    v : 'a or_bottom;
    initialized : bool;
    escaping : bool;
  }
  module Flagged_Value :
    sig
      val bottom : 'Eval.flagged_value
      val equal :
        ('-> '-> bool) ->
        'Eval.flagged_value -> 'Eval.flagged_value -> bool
      val join :
        ('-> '-> 'a) ->
        'Eval.flagged_value ->
        'Eval.flagged_value -> 'Eval.flagged_value
      val pretty :
        (Stdlib.Format.formatter -> '-> unit) ->
        Stdlib.Format.formatter -> 'Eval.flagged_value -> unit
    end
  type ('a, 'origin) record_val = {
    value : 'Eval.flagged_value;
    origin : 'origin option;
    reductness : Eval.reductness;
    val_alarms : Alarmset.t;
  }
  type 'a record_loc = {
    loc : 'a;
    typ : Cil_types.typ;
    loc_alarms : Alarmset.t;
  }
  module type Valuation =
    sig
      type t
      type value
      type origin
      type loc
      val empty : Eval.Valuation.t
      val find :
        Eval.Valuation.t ->
        Cil_types.exp ->
        (Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val or_top
      val add :
        Eval.Valuation.t ->
        Cil_types.exp ->
        (Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
        Eval.Valuation.t
      val fold :
        (Cil_types.exp ->
         (Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
         '-> 'a) ->
        Eval.Valuation.t -> '-> 'a
      val find_loc :
        Eval.Valuation.t ->
        Cil_types.lval -> Eval.Valuation.loc Eval.record_loc or_top
      val remove : Eval.Valuation.t -> Cil_types.exp -> Eval.Valuation.t
      val remove_loc : Eval.Valuation.t -> Cil_types.lval -> Eval.Valuation.t
    end
  module Clear_Valuation :
    functor (Valuation : Valuation->
      sig
        val clear_englobing_exprs :
          Eval.Valuation.t ->
          expr:Cil_types.exp -> subexpr:Cil_types.exp -> Eval.Valuation.t
      end
  type 'loc left_value = {
    lval : Cil_types.lval;
    lloc : 'loc;
    ltyp : Cil_types.typ;
  }
  type ('loc, 'value) assigned =
      Assign of 'value
    | Copy of 'loc Eval.left_value * 'value Eval.flagged_value
  val value_assigned : ('loc, 'value) Eval.assigned -> 'value or_bottom
  type 'location logic_dependency = {
    term : Cil_types.identified_term;
    direct : bool;
    location : 'location option;
  }
  type 'location logic_assign =
      Assigns of Cil_types.identified_term *
        'location Eval.logic_dependency list
    | Allocates of Cil_types.identified_term
    | Frees of Cil_types.identified_term
  type ('loc, 'value) argument = {
    formal : Cil_types.varinfo;
    concrete : Cil_types.exp;
    avalue : ('loc, 'value) Eval.assigned;
  }
  type call_site = Cil_types.kernel_function * Cil_types.kinstr
  type callstack = Eval.call_site list
  type ('loc, 'value) call = {
    kf : Cil_types.kernel_function;
    callstack : Eval.callstack;
    arguments : ('loc, 'value) Eval.argument list;
    rest : (Cil_types.exp * ('loc, 'value) Eval.assigned) list;
    return : Cil_types.varinfo option;
  }
  type recursion = {
    depth : int;
    substitution : (Cil_types.varinfo * Cil_types.varinfo) list;
    base_substitution : Base.substitution;
    withdrawal : Cil_types.varinfo list;
    base_withdrawal : Base.Hptset.t;
  }
  type cacheable = Cacheable | NoCache | NoCacheCallers
end