Module Recursion

module Recursion: sig .. end

Handling of recursion cycles in the callgraph


val get_spec : Cil_types.kinstr -> Cil_types.kernel_function -> Cil_types.funspec
val make : ('v, 'loc) Eval.call -> Eval.recursion option

Creates the information about a recursive call.

val revert : Eval.recursion -> Eval.recursion

Changes the information about a recursive call to be used at the end of the call.