package frama-c

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

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.

exception AddError

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

exception CallStatement

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

exception Not_equal

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

module Signature : sig ... end

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

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

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