package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. L
    Loïc Correnson
  16. J
    Julien Crétin
  17. P
    Pascal Cuoq
  18. Z
    Zaynah Dargaye
  19. B
    Basile Desloges
  20. J
    Jean-Christophe Filliâtre
  21. P
    Philippe Herrmann
  22. M
    Maxime Jacquemin
  23. F
    Florent Kirchner
  24. A
    Alexander Kogtenkov
  25. R
    Remi Lazarini
  26. T
    Tristan Le Gall
  27. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-pdg.core/Pdg/Api/index.html

Module Pdg.ApiSource

Program Dependence Graph type

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).

Sourceexception Bottom

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.

Sourceexception Top

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.

Sourceval from_same_fun : t -> t -> bool

Finding PDG nodes

Get the node corresponding the declaration of a local variable or a formal parameter.

  • raises Not_found

    if the variable is not declared in this function.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_ret_output_node : t -> Pdg_types.PdgTypes.Node.t

Get the node corresponding return stmt.

  • raises Not_found

    if the output state in unreachable

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Get the nodes corresponding to a call output key in the called pdg.

  • raises Not_found

    if the output state in unreachable

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_input_node : t -> int -> Pdg_types.PdgTypes.Node.t

Get the node corresponding to a given input (parameter).

  • raises Not_found

    if the number is not an input number.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_all_inputs_nodes : t -> Pdg_types.PdgTypes.Node.t list

Get the nodes corresponding to all inputs. node_key can be used to know their numbers.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Get the node corresponding to the statement. It shouldn't be a call statement. See also find_simple_stmt_nodes or find_call_stmts.

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

  • raises PdgIndex.CallStatement

    if the given stmt is a function call.

Sourceval 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)

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Get the node corresponding to the label.

  • raises Not_found

    if the given label is not in the PDG.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval 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.

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_top_input_node : t -> Pdg_types.PdgTypes.Node.t
  • raises Not_found

    if there is no top input in the PDG.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_entry_point_node : t -> Pdg_types.PdgTypes.Node.t

Find the node that represent the entry point of the function, i.e. the higher level block.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval 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.

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_location_nodes_at_end : t -> Frama_c_kernel.Locations.Zone.t -> t_nodes_and_undef

Same than find_location_nodes_at_stmt for the program point located at the end of the function.

  • raises Not_found

    if the output state is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_location_nodes_at_begin : t -> Frama_c_kernel.Locations.Zone.t -> t_nodes_and_undef

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.

  • raises Not_found

    if the output state is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Find the call statements to the function (can maybe be somewhere else).

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval find_call_input_node : t -> Frama_c_kernel.Cil_types.stmt -> int -> Pdg_types.PdgTypes.Node.t
  • raises Not_found

    if the call is unreachable or has no such input.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

  • raises Not_found

    if the call is unreachable or has no output node.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

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 globally None, it means that we were not able to compute this information.
  • raises Not_found

    if the statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to find_code_annot_nodes (no control dependencies nodes)

Similar to find_fun_precond_nodes

Sourceval 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. *

find_call_out_nodes_to_select pdg_called called_selected_nodes pdg_caller call_stmt

  • returns

    the call outputs nodes out such that find_output_nodes pdg_called out_key intersects called_selected_nodes.

Sourceval 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

  • returns

    the called input nodes such that the corresponding nodes in the caller intersect caller_selected_nodes

  • raises Not_found

    if the statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Dependencies

Get the nodes to which the given node directly depend on.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_dpds, but for control dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_dpds, but for data dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_dpds, but for address dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Transitive closure of direct_dpds for all the given nodes.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval all_data_dpds : t -> Pdg_types.PdgTypes.Node.t list -> Pdg_types.PdgTypes.Node.t list

Gives the data dependencies of the given nodes, and recursively, all the dependencies of those nodes (regardless to their kind).

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval all_ctrl_dpds : t -> Pdg_types.PdgTypes.Node.t list -> Pdg_types.PdgTypes.Node.t list

Similar to all_data_dpds for control dependencies.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval all_addr_dpds : t -> Pdg_types.PdgTypes.Node.t list -> Pdg_types.PdgTypes.Node.t list

Similar to all_data_dpds for address dependencies.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

build a list of all the nodes that have direct dependencies on the given node.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_uses, but for control dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_uses, but for data dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Similar to direct_uses, but for address dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

build a list of all the nodes that have dependencies (even indirect) on the given nodes.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

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.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Sourceval iter_nodes : (Pdg_types.PdgTypes.Node.t -> unit) -> t -> unit

apply a given function to all the PDG nodes

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

Printers

Sourceval extract : t -> string -> unit

Pretty print pdg into a dot file.

Sourceval pretty_node : bool -> Format.formatter -> Pdg_types.PdgTypes.Node.t -> unit

Pretty print information on a node : with short=true, only the id of the node is printed..

Pretty print information on a node key

Sourceval pretty : ?bw:bool -> Format.formatter -> t -> unit

For debugging... Pretty print pdg information. Print codependencies rather than dependencies if bw=true.

Sourcemodule Marks : module type of Marks
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