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