package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Ordered_stmt/index.html

Module `Frama_c_kernel.Ordered_stmt`

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

val to_ordered : stmt_to_ordered -> Cil_types.stmt -> ordered_stmt

Conversion functions between stmt and ordered_stmt.

val to_stmt : ordered_to_stmt -> ordered_stmt -> Cil_types.stmt

val get_conversion_tables : 
  Cil_types.kernel_function ->
  stmt_to_ordered * ordered_to_stmt * int ordered_stmt_array

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