Module Recursion

module Recursion: sig .. end

val is_recursive_call : Cil_types.kernel_function -> bool

Given the current state of the call stack, detect whether the given given function would start a recursive cycle.

val empty_spec_for_recursive_call : Cil_types.kernel_function -> Cil_types.spec

Generate an empty spec assigns \nothing or assigns \result \from \nothing, to be used to "approximate" the results of a recursive call.