Functor Interpreted_automata.BackwardAnalysis

module BackwardAnalysis: 
functor (D : Domain-> DataflowAnalysis with type state = D.t

Backward dataflow analysis. The domain must provide a backward transfer function that computes the state before a transition from the state after.

Parameters:
D : Domain

type state 
type result 
val fixpoint : ?wto:Interpreted_automata.wto ->
Cil_types.kernel_function ->
state ->
result
module Result: sig .. end