module Recursion:sig
..end
Recursion
val is_recursive_call : Cil_types.kernel_function -> bool
val empty_spec_for_recursive_call : Cil_types.kernel_function -> Cil_types.spec
assigns \nothing
or
assigns \result \from \nothing
, to be used to "approximate" the
results of a recursive call.