Frama-C:
Plug-ins:
Libraries:

Frama-C API - Oneret

type callback = 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.

  • since 20.0-Calcium
  • raises 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.

The ~callback, when provided, is invoked with all the original returns clauses and their associated annotation on inserted gotos.