package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c.kernel/Frama_c_kernel/Oneret/index.html

Module `Frama_c_kernel.Oneret`

type returns_clause =
  Cil_types.stmt * Cil_types.behavior * Cil_types.identified_predicate

type goto_annot = Cil_types.stmt * Cil_types.code_annotation

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.