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