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-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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.

Source

val all_call_out_nodes : 
  callee:Pdg.Api.t ->
  caller:Pdg.Api.t ->
  Frama_c_kernel.Cil_types.stmt ->
  call_interface

all_call_out_nodes ~callee ~caller stmt find all the nodes of callee that define the Call/Out nodes of caller for the call to callee that occurs at stmt. Each such out node is returned, with the set of nodes that define it in callee