sig
  val is_recursive_call : Cil_types.kernel_function -> bool
  val empty_spec_for_recursive_call :
    Cil_types.kernel_function -> Cil_types.spec
end