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
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
module State: sig .. end
module BackwardScope: 
functor (X : sig
val modified : Cil_types.stmt -> bool
end) -> sig .. end
val backward_data_scope : 'a ->
StmtSetLattice.t ->
Cil_types.stmt ->
Cil_types.kernel_function -> Cil_types.stmt -> State.t
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 ->
(Cil_types.stmt -> State.t) * (Cil_types.stmt -> State.t)
val add_s : Cil_datatype.Stmt.Hptset.elt ->
Cil_datatype.Stmt.Hptset.t -> Cil_datatype.Stmt.Hptset.t
val find_scope : Cil_datatype.Stmt.Hptset.elt list ->
StmtSetLattice.t ->
Cil_types.stmt ->
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_types.stmt ->
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
module CA_Map: Cil_datatype.Code_annotation.Map
type proven = (Cil_types.stmt * Cil_types.code_annotation * Cil_types.stmt) CA_Map.t 
Type of the properties proven so far. A binding ca -> (stmt_ca, ca_because, stmt_because) must be read as "ca at statement stmt_ca is a logical consequence of ca_because at statement stmt_because". Currently, ca and ca_because are always exactly the same ACSL assertion, although this may be extended in the future.
val list_proven : proven -> CA_Map.key list
Assertions proven so far, as a list
val add_proven_annot : CA_Map.key * 'a ->
'b * 'c -> ('a * 'b * 'c) CA_Map.t -> ('a * 'b * 'c) CA_Map.t * bool
add_proven_annot proven because add the fact that proven is proven thanks to because. This function also returns a boolean indicating that proven was not already proven.
val check_stmt_annots : Cil_types.code_annotation * 'a ->
Cil_types.stmt ->
(Cil_types.stmt * Cil_types.code_annotation * 'a) CA_Map.t ->
(Cil_types.stmt * Cil_types.code_annotation * 'a) CA_Map.t
Check if an assertion at stmt is identical to ca (itself emitted at stmt_ca). Add them to acc if any
val get_prop_scope_at_stmt : Kernel_function.t ->
Cil_datatype.Stmt.t ->
Cil_types.code_annotation -> Cil_datatype.Stmt.Hptset.t * CA_Map.key list
Return the set of stmts (scope) where annot has the same value as at stmt, and adds to proven the annotations that are identical to annot at statements that are both in scope and dominated by stmt. stmt is not added to the set, and annot is not added to proven.
class check_annot_visitor : object .. end
Collect the annotations that can be removed because they are redondant.
val f_check_asserts : unit ->
(Cil_datatype.Stmt.t * Cil_types.code_annotation * Cil_datatype.Stmt.t)
CA_Map.t
val check_asserts : unit -> CA_Map.key list
val get_prop_scope_at_stmt : Kernel_function.t ->
Cil_datatype.Stmt.t ->
Cil_types.code_annotation -> Cil_datatype.Stmt.Hptset.t * CA_Map.key list
val emitter : Emitter.t lazy_t
val rm_asserts : unit -> unit
Mark as proved the annotations collected by check_asserts.