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 BACKWARD_MONOTONE_PARAMETER =sig
..end
module Simple_backward:
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_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
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
.