sig
  val get_spec :
    Cil_types.kinstr -> Cil_types.kernel_function -> Cil_types.funspec
  val make : ('v, 'loc) Eval.call -> Eval.recursion option
  val revert : Eval.recursion -> Eval.recursion
end