Index of modules

C
Callwise

Computation of callwise functional dependencies.

D
Deps [Function_Froms]
DepsOrUnassigned [Function_Froms]
F
ForceCallDeps [From_parameters]

Option -calldeps.

ForceDeps [From_parameters]

Option -deps

From

No function is directly exported: they are registered in Db.From.

From_compute

Module implementing the computation of functional dependencies

From_parameters
From_register

Registration of the From plugin in Frama-C main loop.

From_register_gui

Extension of the GUI in order to support the from analysis.

Function_Froms

Datastructures and common operations for the results of the From plugin.

Functionwise

Computation of functional dependencies.

M
Make [From_compute]

Functor computing the functional dependencies, according to the three modules above.

Memory [Function_Froms]
S
ShowIndirectDeps [From_parameters]

Option -show-indirect-deps

V
VerifyAssigns [From_parameters]

Option -from-verify-assigns.