Module Datascope

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
type t 
val pretty : Format.formatter -> t -> unit
end) -> sig .. end
Place to store the dataflow analyses results
module States: GenStates(State)
module BackwardScope: 
functor (X : sig
val modified : Cil_types.stmt -> bool
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
val modified : Cil_types.stmt -> bool
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 :
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.