Module CtrlDpds.PdgPostdom

module PdgPostdom: sig .. end
This backward dataflow implements a variant of postdominators that verify the property P enunciated in bts 963: a statement postdominates itself if and only it is within the main path of a syntactically infinite loop.

The implementation is as follows:



type t = State.t Cil_datatype.Stmt.Hashtbl.t 
val compute : Kernel_function.t -> State.t Cil_datatype.Stmt.Hashtbl.t
val get : State.t Cil_datatype.Stmt.Hashtbl.t ->
with_s:bool ->
Cil_datatype.Stmt.Hashtbl.key -> bool * Cil_datatype.Stmt.Hptset.t