module Oneret:sig..end
typereturns_clause =Cil_types.stmt * Cil_types.behavior * Cil_types.identified_predicate
typegoto_annot =Cil_types.stmt * Cil_types.code_annotation
typecallback =returns_clause -> goto_annot list -> unit
val encapsulate_local_vars : Cil_types.fundec -> unitIf there are local variables with destructors belonging to the main block
of f, encapsulate_local_vars f will move ret, the return
statement of f outside of this main block (changing f.sbody to
a two-statement block composed of the old block and ret) to
avoid having gotos to ret bypassing the initialization of these variables.
This function assumes that Oneret.oneret has already been run on f,
i.e. that there is exactly one return statement in there.
Abort.fatal if the function is not defined.val oneret : ?callback:callback -> Cil_types.fundec -> unitMake sure that there is only one Return statement in the whole body. Replace all the other returns with Goto. Make sure that there is a return if the function is supposed to return something, and it is not declared to not return.
~callback, when provided,
is invoked with all the original returns clauses and their associated
annotation on inserted gotos.