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.

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