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 -> unit
If 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 -> unit
Make 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.