module Dataflows:sig
..end
module type FUNCTION_ENV =sig
..end
val function_env : Cil_types.kernel_function -> (module Dataflows.FUNCTION_ENV)
module type JOIN_SEMILATTICE =sig
..end
module type FORWARD_MONOTONE_PARAMETER =sig
..end
module Simple_forward:
val transfer_if_from_guard : (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
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