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