sig
  type state
  type value
  type location
  val assign :
    Transfer_stmt.S.state ->
    Cil_types.kinstr ->
    Cil_types.lval -> Cil_types.exp -> Transfer_stmt.S.state Eval.or_bottom
  val assume :
    Transfer_stmt.S.state ->
    Cil_types.stmt ->
    Cil_types.exp -> bool -> Transfer_stmt.S.state Eval.or_bottom
  val call :
    Cil_types.stmt ->
    Cil_types.lval option ->
    Cil_types.exp ->
    Cil_types.exp list ->
    Transfer_stmt.S.state ->
    Transfer_stmt.S.state list Eval.or_bottom * Value_types.cacheable
  val check_unspecified_sequence :
    Cil_types.stmt ->
    Transfer_stmt.S.state ->
    (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
     Cil_types.lval list * Cil_types.stmt Stdlib.ref list)
    list -> unit Eval.or_bottom
  val enter_scope :
    Cil_types.kernel_function ->
    Cil_types.varinfo list -> Transfer_stmt.S.state -> Transfer_stmt.S.state
  type call_result = {
    states : Transfer_stmt.S.state list Eval.or_bottom;
    cacheable : Value_types.cacheable;
    builtin : bool;
  }
  val compute_call_ref :
    (Cil_types.stmt ->
     (Transfer_stmt.S.location, Transfer_stmt.S.value) Eval.call ->
     Transfer_stmt.S.state -> Transfer_stmt.S.call_result)
    Stdlib.ref
end