module Datascope:sig
..end
val get_data_scope_at_stmt : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_datatype.Stmt.Hptset.t *
(Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t)
Kernel_function.No_Definition
if kf
has no definition.lval
before stmt
:val get_prop_scope_at_stmt : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list
compute the set of statements where the given annotation has the same value as before the given stmt. Also returns the eventual code annotations that are implied by the one given as argument.
val check_asserts : unit -> Cil_types.code_annotation list
Print how many assertions could be removed based on the previous
analysis (get_prop_scope_at_stmt
) and return the annotations
that can be removed.
val rm_asserts : unit -> unit
Same analysis than check_asserts
but mark the assertions as proven.