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 '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 unop_context = Cil_types.exp * Cil_types.exp
  type binop_context =
      Cil_types.exp * Cil_types.exp * Cil_types.exp * Cil_types.typ
  type index_context =
      Cil_types.exp * Cil_types.offset * Cil_types.typ * Cil_types.exp option
  type reductness = Unreduced | Reduced | Created | Dull
  type 'a flagged_value = { v : 'a; initialized : bool; escaping : bool; }
  type ('a, 'origin) record_val = {
    value : 'a or_bottom 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 filter :
        (Cil_types.exp ->
         (Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
         bool) ->
        (Cil_types.lval -> Eval.Valuation.loc Eval.record_loc -> bool) ->
        Eval.Valuation.t -> Eval.Valuation.t
    end
  module Clear_Valuation :
    functor (Valuation : Valuation->
      sig
        val clear_expr :
          Eval.Valuation.t -> Cil_types.exp -> Eval.Valuation.t
      end
  type 'loc left_value = {
    lval : Cil_types.lval;
    lloc : 'loc;
    ltyp : Cil_types.typ;
  }
  type 'value copied =
      Determinate of 'value Eval.flagged_value
    | Exact of 'value or_bottom Eval.flagged_value
  type 'value assigned =
      Assign of 'value
    | Copy of Cil_types.lval * 'value Eval.copied
  val value_assigned : 'value Eval.assigned -> 'value or_bottom
  type 'value argument = {
    formal : Cil_types.varinfo;
    concrete : Cil_types.exp;
    avalue : 'value Eval.assigned;
  }
  type 'value call = {
    kf : Cil_types.kernel_function;
    arguments : 'value Eval.argument list;
    rest : (Cil_types.exp * 'value Eval.assigned) list;
  }
  type ('state, 'summary, 'value) return = {
    post_state : 'state;
    returned_value : 'value or_bottom Eval.flagged_value option;
    summary : 'summary;
  }
  type ('state, 'summary, 'value) call_result =
      ('state, 'summary, 'value) Eval.return list or_bottom
  type 't init =
      Default
    | Continue of 't
    | Custom of (Cil_types.stmt * 't) list
  type ('state, 'summary, 'value) action =
      Compute of 'state Eval.init * bool
    | Recall of 'state Eval.init
    | Result of ('state, 'summary, 'value) Eval.call_result *
        Value_types.cacheable
  exception InvalidCall
end