package frama-c

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

An ordered_stmt is an int representing a stmt in a particular function. They are sorted by the topological ordering of stmts (s1 < s2 if s1 precedes s2, or s2 does not precede s1); they are contiguous and start from 0.

Note: due to the presence of unreachable statements in the graph, you should not assume that the entry point is statement number 0 and the return is statement number |nb_stmts - 1|. Use Kernel_function.find_first_stmt and Kernel_function.find_return instead.

type 'a ordered_stmt_array = 'a array

As ordered_stmts are contiguous and start from 0, they are suitable for use by index in a array. This type denotes arrays whose index are ordered stmts.

type ordered_to_stmt = Cil_types.stmt ordered_stmt_array

Types of conversion tables between stmt and ordered_stmt.

type stmt_to_ordered

Conversion functions between stmt and ordered_stmt.

This function computes, caches, and returns the conversion tables between a stmt and an ordered_stmt, and a table mapping each ordered_stmt to a connex component number (connex component number are also sorted in topological order

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