Module Dataflows

module Dataflows: sig .. end
Implementation of data flow analyses over user-supplied domains.

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

Backward dataflow


module type BACKWARD_MONOTONE_PARAMETER = sig .. end
Statement-based backward dataflow.
module Simple_backward: 
functor (Fenv : FUNCTION_ENV) ->
functor (P : BACKWARD_MONOTONE_PARAMETER) -> sig .. end

Forward dataflow


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

Helper functions for forward dataflow.


val transfer_if_from_guard : (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
transfer_if_from_guard implements FORWARD_MONOTONE_PARAMETER.transfer_stmt for the If statement, given a function transfer_guard.

transfer_guard receives a conditional expression, the current statement, and the current state, and must return two states in which the conditional is assumed to be true and false respectively. Returning twice the current state is a valid, albeit imprecise, result.

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. The same function transfer_guard can be used for transfer_if_from_guard and transfer_switch_from_guard.