Module CtrlDpds.Lexical_successors

module Lexical_successors: sig .. end
Compute a graph which provide the lexical successor of each statement s, ie. the statement which is the next one if 's' is replaced by Nop. Notice that if 's' is an If, Loop, ... the considered statement is the whole block.

Example : (1) x = 3; (2) if (c) (3) y = 3; (4) goto L; else (5) z = 8; (6) while (c--) (7) x++; (8) L : return x;

(1) -> (2) -> (6) -> (8) (3) -> (4) -> (6) (5) -> (6) (7) -> (6)


type t = Cil_types.stmt Cil_datatype.Stmt.Hashtbl.t 
Type of the graph
val compute : Kernel_function.t -> Cil_datatype.Stmt.t Cil_datatype.Stmt.Hashtbl.t
Compute the lexical successor graph for function kf
val find : 'a Cil_datatype.Stmt.Hashtbl.t -> Cil_datatype.Stmt.Hashtbl.key -> 'a
Raises Not_found if 'stmt' has no successor in 'graph' ie when it is return.
Returns the lexical successor of stmt in graph.