sig
module type FUNCTION_ENV =
sig
val to_ordered : Cil_types.stmt -> Ordered_stmt.ordered_stmt
val to_stmt : Ordered_stmt.ordered_stmt -> Cil_types.stmt
val nb_stmts : int
val kf : Kernel_function.t
end
val function_env :
Cil_types.kernel_function -> (module Dataflows.FUNCTION_ENV)
module type JOIN_SEMILATTICE =
sig
type t
val join :
Dataflows.JOIN_SEMILATTICE.t ->
Dataflows.JOIN_SEMILATTICE.t -> Dataflows.JOIN_SEMILATTICE.t
val bottom : Dataflows.JOIN_SEMILATTICE.t
val join_and_is_included :
Dataflows.JOIN_SEMILATTICE.t ->
Dataflows.JOIN_SEMILATTICE.t -> Dataflows.JOIN_SEMILATTICE.t * bool
val pretty : Format.formatter -> Dataflows.JOIN_SEMILATTICE.t -> unit
end
module type FORWARD_MONOTONE_PARAMETER =
sig
type t
val join : t -> t -> t
val bottom : t
val join_and_is_included : t -> t -> t * bool
val pretty : Format.formatter -> t -> unit
val transfer_stmt : Cil_types.stmt -> t -> (Cil_types.stmt * t) list
val init : (Cil_types.stmt * t) list
end
module Simple_forward :
functor (Fenv : FUNCTION_ENV) ->
functor (P : FORWARD_MONOTONE_PARAMETER) ->
sig
val before : P.t Ordered_stmt.ordered_stmt_array
val fold_on_result :
('a -> Cil_types.stmt -> P.t -> 'a) -> 'a -> 'a
val iter_on_result : (Cil_types.stmt -> P.t -> unit) -> unit
end
val transfer_if_from_guard :
(Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
val transfer_switch_from_guard :
(Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
Cil_types.stmt -> 'a -> (Cil_types.stmt * 'a) list
end