module Datascope: sig
.. end
The aim here is to select the statements where a data D
has the same value then a given starting program point L.
module R: Plugin.Register
(
sig
val name : string
val shortname : string
val help : string
end
)
val cat_rm_asserts_name : string
val cat_rm_asserts : Log.category
Computing a mapping between zones and modifying statements
We first go through all the function statements in other to build
a mapping between each zone and the statements that are modifying it.
module StmtDefault: sig
.. end
Statement identifier
module StmtSetLattice: sig
.. end
set of values to store for each data
module InitSid: sig
.. end
A place to map each data to the state of statements that modify it.
val get_lval_zones : for_writing:bool ->
Cil_types.stmt ->
Cil_types.lval -> Locations.Zone.t * bool * Locations.Zone.t
val register_modified_zones : InitSid.LM.t ->
StmtSetLattice.O.elt -> InitSid.LM.t
Add to stmt
to lmap
for all the locations modified by the statement.
Something to do only for calls and assignments.
val compute : Kernel_function.t -> Cil_types.stmt list * InitSid.LM.t
compute the mapping for the function
Raises Kernel_function.No_Definition
if kf
has no definition
Computing Scopes
module State: sig
.. end
module GenStates: functor (
S
:
sig
end
) ->
sig
.. end
Place to store the dataflow analyses results
module States: GenStates
(
State
)
module BackwardScope: functor (
X
:
sig
end
) ->
sig
.. end
val backward_data_scope : Cil_datatype.Stmt.Hashtbl.key list ->
StmtSetLattice.t -> Cil_datatype.Stmt.Hashtbl.key -> unit
module ForwardScope: functor (
X
:
sig
end
) ->
sig
.. end
val forward_data_scope : StmtSetLattice.t ->
Cil_types.stmt ->
Cil_types.kernel_function ->
('a -> Cil_types.stmt -> State.t -> 'a) -> 'a -> 'a
val add_s : Cil_datatype.Stmt.Hptset.elt ->
Cil_datatype.Stmt.Hptset.t -> Cil_datatype.Stmt.Hptset.t
val find_scope : Cil_datatype.Stmt.Hashtbl.key list ->
StmtSetLattice.t ->
Cil_datatype.Stmt.Hashtbl.key ->
Cil_types.kernel_function ->
Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t *
Cil_datatype.Stmt.Hptset.t
Do backward and then forward propagations and compute the 3 statement sets :
- forward only,
- forward and backward,
- backward only.
val get_data_scope_at_stmt : Kernel_function.t ->
Cil_datatype.Stmt.Hashtbl.key ->
Cil_types.lval ->
Cil_datatype.Stmt.Hptset.t *
(Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t)
Try to find the statement set where data
has the same value than
before stmt
.
Raises Kernel_function.No_Definition
if kf
has no definition
exception ToDo
val get_annot_zone : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Locations.Zone.t
val add_annot : Cil_types.code_annotation ->
Cil_types.code_annotation list -> Cil_types.code_annotation list * bool
add annot
to acc
if it is not already in.
acc
is supposed to be sorted according to annot_id
.
Returns true if it has been added.
val check_stmt_annots : Cil_types.predicate Cil_types.named ->
Cil_types.stmt ->
Cil_types.code_annotation list -> Cil_types.code_annotation list
Check if some assertions before s
are identical to pred
.
Add them to acc if any
val get_prop_scope_at_stmt : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list
Return the set of stmts (scope) where annot
has the same value
than in stmt
and add to to_be_removed
the annotations that are identical to annot
in the statements that are both the scope and that are dominated by stmt.
class check_annot_visitor :
object
.. end
Collect the annotations that can be removed because they are redondant.
val f_check_asserts : unit -> Cil_types.code_annotation list
val check_asserts : unit -> Cil_types.code_annotation list
val get_prop_scope_at_stmt : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list
class rm_annot_visitor : Cil_types.code_annotation list ->
object
.. end
Visitor to remove the annotations collected by check_asserts
.
val rm_asserts : unit -> unit
Remove the annotations collected by check_asserts
.