sig
  val current_kf_inout : unit -> Inout_type.t option
  module type S =
    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
  module Make :
    functor (Abstract : Abstractions.Eva->
      sig
        type state = Abstract.Dom.t
        type value = Abstract.Val.t
        type location = Abstract.Loc.location
        val assign :
          state ->
          Cil_types.kinstr ->
          Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
        val assume :
          state ->
          Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
        val call :
          Cil_types.stmt ->
          Cil_types.lval option ->
          Cil_types.exp ->
          Cil_types.exp list ->
          state -> state list Eval.or_bottom * Value_types.cacheable
        val check_unspecified_sequence :
          Cil_types.stmt ->
          state ->
          (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
           Cil_types.lval list * Cil_types.stmt ref list)
          list -> unit Eval.or_bottom
        val enter_scope :
          Cil_types.kernel_function ->
          Cil_types.varinfo list -> state -> state
        type call_result = {
          states : state list Eval.or_bottom;
          cacheable : Value_types.cacheable;
          builtin : bool;
        }
        val compute_call_ref :
          (Cil_types.stmt ->
           (location, value) Eval.call -> state -> call_result)
          ref
      end
end