Module Dataflows

module Dataflows: sig .. end
Set of dataflow frameworks. Instead of defining a single dataflow interface that tries to accomodate with all the options, having a set of dataflows allow to keep things simple in the general case; specific demands are handled by using more general dataflows. Simpler-to-instanciate dataflows are instances of the more general dataflows.

module type FUNCTION_ENV = sig .. end
Environment relative to the function being processed, and function to create them from Kf.
val function_env : Cil_types.kernel_function -> (module Dataflows.FUNCTION_ENV)
module type JOIN_SEMILATTICE = sig .. end
module type FORWARD_MONOTONE_PARAMETER = sig .. end
Edge-based forward dataflow.
module Simple_forward: 
functor (Fenv : FUNCTION_ENV) ->
functor (P : FORWARD_MONOTONE_PARAMETER) -> sig .. end
val transfer_if_from_guard : (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
The following functions allow implementing transfer_stmt for the If statement, from a transfer_guard function.

transfer_guard receives a conditional expression, the current statement, and the current state, and returns the new state when the expression evaluates to respectively true and false.

val transfer_switch_from_guard : (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
Same as Dataflows.transfer_if_from_guard, but for a Switch statement.