module BackwardAnalysis:
Backward dataflow analysis. The domain must provide a backward transfer
function that computes the state before a transition from the state after.
Parameters: |
|
type
state
type
result
val fixpoint : ?wto:Interpreted_automata.wto ->
Cil_types.kernel_function ->
state ->
result
module Result:sig
..end