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:
- compute postdominators with an additional flag infinite loop/non-infinite
loop. Every path that may terminate does not have the "infinite loop" flag
- the implementation verifies property P only for Loop statements. To
obtain the property, the cfg is locally rewritten. For statements
--> p --> s:Loop --> h --> ... --> e
^ |
| |
--------------------------
the edges p --> s are transformed into p --> h, but _not_ the backward
edges e --> s. This way, s post-dominates itself if and only if s is
a syntactically infinite loop, but not if there is an outgoing edge.
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