sig
  type 'a or_bottom = [ `Bottom | `Value of 'a ]
  val ( >>- ) : 'a or_bottom -> ('-> 'b or_bottom) -> 'b or_bottom
  val ( >>-: ) : 'a or_bottom -> ('-> 'b) -> 'b or_bottom
  type 'a or_top = [ `Top | `Value of 'a ]
  type 'a or_top_or_bottom = [ `Bottom | `Top | `Value of 'a ]
  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 :
        (Format.formatter -> '-> unit) ->
        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
        Eval.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 Eval.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 logic_assign =
      Assigns of Cil_types.from
    | 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 ('loc, 'value) call = {
    kf : Cil_types.kernel_function;
    arguments : ('loc, 'value) Eval.argument list;
    rest : (Cil_types.exp * ('loc, 'value) Eval.assigned) list;
    return : Cil_types.varinfo option;
    recursive : bool;
  }
end