module type BackwardsTransfer =sig
..end
val name : string
val debug : bool Pervasives.ref
type
t
val pretty : Format.formatter -> t -> unit
val funcExitData : t
val combineStmtStartData : Cil_types.stmt ->
old:t ->
t -> t option
val combineSuccessors : t ->
t -> t
val doStmt : Cil_types.stmt -> t Dataflow.action
(Cil.CurrentLoc.get
())
is set before calling this. If it returns None, then we have some
default handling. Otherwise, the returned data is the data before the
branch (not considering the exception handlers)val doInstr : Cil_types.stmt ->
Cil_types.instr ->
t -> t Dataflow.action
(Cil.CurrentLoc.get ())
is set before calling this. If it returns None,
then we have some default handling. Otherwise, the returned data is the
data before the branch (not considering the exception handlers)val filterStmt : Cil_types.stmt -> Cil_types.stmt -> bool
val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool
true
if there is a path in the control-flow graph of the
function from the first statement to the second. Used to choose a "good"
node in the worklist.
Suggested use is let stmt_can_reach = Stmts_graph.stmt_can_reach kf
,
where kf
is the kernel_function being analyzed;
let stmt_can_reach _ _ = true
is also correct, albeit less efficient
Since Oxygen-20120901
module StmtStartData:Dataflow.StmtStartData
with type data = t