package frama-c

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

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

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

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

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

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

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

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

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)

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

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.

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

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

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

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.

  • raises Not_found

    if the given statement is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

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

val 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 Not_found

    if the call is unreachable.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

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

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

  • returns

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

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

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

val direct_ctrl_dpds : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

Similar to direct_dpds, but for control dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

val direct_data_dpds : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

Similar to direct_dpds, but for data dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

val direct_addr_dpds : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

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.

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

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

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

val direct_ctrl_uses : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

Similar to direct_uses, but for control dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

val direct_data_uses : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

Similar to direct_uses, but for data dependencies only.

  • raises Bottom

    if given PDG is bottom.

  • raises Top

    if the given pdg is top.

val direct_addr_uses : t -> Pdg_types.PdgTypes.Node.t -> Pdg_types.PdgTypes.Node.t list

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.

val 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

val extract : t -> string -> unit

Pretty print pdg into a dot file.

val pretty_node : bool -> Stdlib.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..

val pretty_key : Stdlib.Format.formatter -> Pdg_types.PdgIndex.Key.t -> unit

Pretty print information on a node key

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

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

module 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