package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-impact.core/Impact/Pdg_aux/index.html

Module `Impact.Pdg_aux`Source

Useful functions that are not directly accessible through the other Pdg modules.

Sourcetype node = Pdg_types.PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t

Refinement of a PDG node: we add an indication of which zone is really impacted

Sourceval pretty_node : node Frama_c_kernel.Pretty_utils.formatter

Sourcemodule NS : sig ... end

Sets of pairs Node.t * Zone.t, with a special semantics for zones: add n z (add n z' empty) results in (n, Zone.join z z') instead of a set with two different elements. All operations see only instance of a node, with the join of all possible zones. Conversely, a node should not be present with an empty zone.

Sourcetype call_interface = (Pdg_types.PdgTypes.Node.t * NS.t) list

Abstract view of a call frontier. An element n, S of the list is such that n is impacted if one of the nodes of S is impacted.

Source

val all_call_input_nodes : 
  caller:Pdg.Api.t ->
  callee:(Frama_c_kernel.Cil_types.kernel_function * Pdg.Api.t) ->
  Frama_c_kernel.Cil_types.stmt ->
  call_interface

all_call_input_nodes caller callee call_stmt find all the nodes above call_stmt in the pdg of caller that define the inputs of callee. Each input node in callee is returned with the set of nodes that define it in caller.