Frama-C API - Ordered_stmt
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.
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_arrayTypes of conversion tables between stmt and ordered_stmt.
val to_ordered : stmt_to_ordered -> Cil_types.stmt -> ordered_stmtConversion functions between stmt and ordered_stmt.
val to_stmt : ordered_to_stmt -> ordered_stmt -> Cil_types.stmtval get_conversion_tables : Cil_types.kernel_function -> stmt_to_ordered * ordered_to_stmt * int ordered_stmt_arrayThis 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