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