module Ordered_stmt:sig
..end
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.
typeordered_stmt =
int
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
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.typeordered_to_stmt =
Cil_types.stmt ordered_stmt_array
type
stmt_to_ordered
val to_ordered : stmt_to_ordered -> Cil_types.stmt -> 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
ordered_stmt
, and a table mapping each
ordered_stmt to a connex component number (connex component number
are also sorted in topological order