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
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
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 :
- forward only,
- forward and backward,
- backward only.
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
.