module Recursion:sig
..end
Handling of recursion cycles in the callgraph
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.