package frama-c

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

Module Pdg_types.PdgIndexSource

This module can be useful to store some information about different elements of a function.

PdgIndex.Signature is used to store information about function inputs/outputs either for the function itself or for its calls. PdgIndex.Key provides keys to identify the different elements we want to speak about. PdgIndex.FctIndex is the main object that manages the stored information.

This module is used for instance to store the relation between a function elements and the nodes of its PDG, but it can also be used to store many other things.

Sourceexception AddError

try to add in information while there is already something stored. Should have used replace function

Sourceexception CallStatement

Some functions do not apply to call statements because the stored information has a different type.

Sourceexception Not_equal

When we compare two things with different locations (no order)

Sourcemodule Signature : sig ... end

What we call a Signature a mapping between keys that represent either a function input or output, and some information.

Sourcemodule Key : sig ... end

The keys can be used to identify an element of a function. Have a look at the type t to know which kind of elements can be identified.

Sourcemodule FctIndex : sig ... end

Mapping between the function elements we are interested in and some information. Used for instance to associate the nodes with the statements, or the marks in a slice.

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