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