package frama-c
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493
doc/frama-c-pdg.core/Pdg/Api/index.html
Module Pdg.Api
Source
Program Dependence Graph type
type t_nodes_and_undef =
(Pdg_types.PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option) list
* Frama_c_kernel.Locations.Zone.t option
type for the return value of many find_xxx
functions when the answer can be a list of (node, z_part)
and an undef zone
. For each node, z_part
can specify which part of the node is used in terms of zone (None
means all).
Raised by most function when the PDG is Bottom because we can hardly do nothing with it. It happens when the function is unreachable because we have no information about it.
Raised by most function when the PDG is Top because we can hardly do nothing with it. It happens when we didn't manage to compute it, for instance for a variadic function.
PDG depedency state
Getters
Get the PDG of a function. Build it if it doesn't exist yet.
Finding PDG nodes
Get the node corresponding the declaration of a local variable or a formal parameter.
Get the node corresponding return stmt.
Get the nodes corresponding to a call output key in the called pdg.
Get the node corresponding to a given input (parameter).
Get the nodes corresponding to all inputs. node_key
can be used to know their numbers.
Get the node corresponding to the statement. It shouldn't be a call statement. See also find_simple_stmt_nodes
or find_call_stmts
.
val find_simple_stmt_nodes :
t ->
Frama_c_kernel.Cil_types.stmt ->
Pdg_types.PdgTypes.Node.t list
Get the nodes corresponding to the statement. It is usually composed of only one node (see find_stmt_node
), except for call statement. Be careful that for block statements, it only returns a node corresponding to the elementary stmt (see find_stmt_and_blocks_nodes
for more)
val find_label_node :
t ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.label ->
Pdg_types.PdgTypes.Node.t
Get the node corresponding to the label.
val find_stmt_and_blocks_nodes :
t ->
Frama_c_kernel.Cil_types.stmt ->
Pdg_types.PdgTypes.Node.t list
Get the nodes corresponding to the statement like find_simple_stmt_nodes
but also add the nodes of the enclosed statements if stmt
contains blocks.
Find the node that represent the entry point of the function, i.e. the higher level block.
val find_location_nodes_at_stmt :
t ->
Frama_c_kernel.Cil_types.stmt ->
before:bool ->
Frama_c_kernel.Locations.Zone.t ->
t_nodes_and_undef
Find the nodes that define the value of the location at the given program point. Also return a zone that might be undefined at that point.
Same than find_location_nodes_at_stmt
for the program point located at the end of the function.
Same than find_location_nodes_at_stmt
for the program point located at the beginning of the function. Notice that it can only find formal argument nodes. The remaining zone (implicit input) is returned as undef.
val find_call_stmts :
Frama_c_kernel.Cil_types.kernel_function ->
caller:Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt list
Find the call statements to the function (can maybe be somewhere else).
val find_call_input_node :
t ->
Frama_c_kernel.Cil_types.stmt ->
int ->
Pdg_types.PdgTypes.Node.t
val find_code_annot_nodes :
t ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
Pdg_types.PdgTypes.Node.t list
* Pdg_types.PdgTypes.Node.t list
* t_nodes_and_undef option
The result is composed of three parts :
- the first part of the result are the control dependencies nodes of the annotation,
- the second part is the list of declaration nodes of the variables used in the annotation;
- the third part is similar to
find_location_nodes_at_stmt
result but for all the locations needed by the annotation. When the third part is globallyNone
, it means that we were not able to compute this information.
val find_fun_precond_nodes :
t ->
Frama_c_kernel.Cil_types.predicate ->
Pdg_types.PdgTypes.Node.t list * t_nodes_and_undef option
Similar to find_code_annot_nodes
(no control dependencies nodes)
val find_fun_postcond_nodes :
t ->
Frama_c_kernel.Cil_types.predicate ->
Pdg_types.PdgTypes.Node.t list * t_nodes_and_undef option
Similar to find_fun_precond_nodes
val find_fun_variant_nodes :
t ->
Frama_c_kernel.Cil_types.term ->
Pdg_types.PdgTypes.Node.t list * t_nodes_and_undef option
Similar to find_fun_precond_nodes
Propagation
See also Pdg.mli
for more function that cannot be here because they use polymorphic types. *
val find_call_out_nodes_to_select :
t ->
Pdg_types.PdgTypes.NodeSet.t ->
t ->
Frama_c_kernel.Cil_types.stmt ->
Pdg_types.PdgTypes.Node.t list
find_call_out_nodes_to_select pdg_called called_selected_nodes pdg_caller call_stmt
val find_in_nodes_to_select_for_this_call :
t ->
Pdg_types.PdgTypes.NodeSet.t ->
Frama_c_kernel.Cil_types.stmt ->
t ->
Pdg_types.PdgTypes.Node.t list
find_in_nodes_to_select_for_this_call pdg_caller caller_selected_nodes call_stmt pdg_called
Dependencies
Get the nodes to which the given node directly depend on.
Similar to direct_dpds
, but for control dependencies only.
Similar to direct_dpds
, but for data dependencies only.
Similar to direct_dpds
, but for address dependencies only.
Transitive closure of direct_dpds
for all the given nodes.
Gives the data dependencies of the given nodes, and recursively, all the dependencies of those nodes (regardless to their kind).
Similar to all_data_dpds
for control dependencies.
Similar to all_data_dpds
for address dependencies.
build a list of all the nodes that have direct dependencies on the given node.
Similar to direct_uses
, but for control dependencies only.
Similar to direct_uses
, but for data dependencies only.
Similar to direct_uses
, but for address dependencies only.
build a list of all the nodes that have dependencies (even indirect) on the given nodes.
custom_related_nodes get_dpds node_list
build a list, starting from the node in node_list
, and recursively add the nodes given by the function get_dpds
. For this function to work well, it is important that get_dpds n
returns a subset of the nodes directly related to n
, ie a subset of direct_uses
U direct_dpds
.
apply a given function to all the PDG nodes
Printers
Pretty print information on a node : with short=true
, only the id of the node is printed..
Pretty print information on a node key
For debugging... Pretty print pdg information. Print codependencies rather than dependencies if bw=true
.