Frama_c_kernel.Dataflow2
Implementation of data flow analyses over user-supplied domains.
type 't action =
| Default | (* The default action *) |
| Done of 't | (* Do not do the default action. Use this result *) |
| Post of 't -> 't | (* The default action, followed by the given * transformer *) |
possible kinds of action for backward analysis
type 't guardaction =
| GDefault | (* The default state *) |
| GUse of 't | (* Use this data for the branch *) |
| GUnreachable | (* The branch will never be taken. *) |
For if statements
module type StmtStartData = sig ... end
module StartData (X : sig ... end) : StmtStartData with type data = X.t
This module can be used to instantiate the StmtStartData
components of the functors below. It is implemented through stmt-indexed hashtables.
module type ForwardsTransfer = sig ... end
Interface to provide for a backward dataflow analysis.
module Forwards (T : ForwardsTransfer) : sig ... end
module type BackwardsTransfer = sig ... end
Interface to provide for a backward dataflow analysis.
module Backwards (T : BackwardsTransfer) : sig ... end
val find_stmts : Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt list