package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct