package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Module to perform dominators and postdominators analyses. This module was completely redesigned and provides many new functions.

A dominator d of s is a statement such that all paths from the entry point of a function to s must go through d.

A postdominator p of s is a statement such that all paths from s to the return point of the function must go through p.

By definition, a statement always (post)dominates itself (except if it is unreachable).

An immediate (post)dominator (or i(post)dom) d is the unique (post)dominator of s that strictly (post)dominates s but is (post)dominated by all other (post)dominators of s.

A common ancestor (or child) of a list of statements is a (post)dominator that (post)dominates all the statements

  • since 30.0-Zinc
val compute_dominators : Cil_types.kernel_function -> unit

Compute the Dominators analysis and register its result.

val compute_postdominators : Cil_types.kernel_function -> unit

Compute the Postdominators analysis and register its result.

Return the set of dominators of the given statement. The empty set means the statement is unreachable.

val get_postdominators : Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Return the set of postdominators of the given statement. The empty set means the statement is unreachable.

val get_strict_dominators : Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Same as get_dominators but exclude the statement itself. The empty set means the statement is unreachable or is only dominated by itself.

val get_strict_postdominators : Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Same as get_postdominators but exclude the statement itself. The empty set means the statement is unreachable or is only post-dominated by itself.

val dominates : Cil_types.stmt -> Cil_types.stmt -> bool

dominates a b return true if a dominates b.

val postdominates : Cil_types.stmt -> Cil_types.stmt -> bool

postdominates a b return true if a postdominates b.

val strictly_dominates : Cil_types.stmt -> Cil_types.stmt -> bool

strictly_dominates a b return true if a strictly dominates b.

val strictly_postdominates : Cil_types.stmt -> Cil_types.stmt -> bool

strictly_postdominates a b return true if a strictly postdominates b.

val get_idom : Cil_types.stmt -> Cil_types.stmt option

Return the immediate dominator of the given statement.

val get_ipostdom : Cil_types.stmt -> Cil_types.stmt option

Return the immediate postdominator of the given statement.

val nearest_common_ancestor : Cil_types.stmt list -> Cil_types.stmt option

Return the closest common ancestor of the given statement list.

  • before 30.0-Zinc

    previous implementation always returned a statement and raised a failed assertion in case of unreachable statement.

val nearest_common_child : Cil_types.stmt list -> Cil_types.stmt option

Return the closest common child of the given statement list.

val pretty_dominators : Stdlib.Format.formatter -> unit -> unit

Print the result of the domination analysis. Each statement is either dominated by a set of statements, or Top if unreachable.

val pretty_postdominators : Stdlib.Format.formatter -> unit -> unit

Print the result of the postdomination analysis. Each statement is either postdominated by a set of statements, or Top if unreachable.

val print_dot_dominators : string -> Cil_types.kernel_function -> unit

Print the domination graph in a file basename.function_name.dot.

val print_dot_postdominators : string -> Cil_types.kernel_function -> unit

Print the postdomination graph in a file basename.function_name.dot.

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