module Scope: sig
.. end
val get_data_scope_at_stmt : (Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_datatype.Stmt.Hptset.t *
(Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t))
Pervasives.ref
Raises Kernel_function.No_Definition
if
kf
has no definition.
Returns 3 statement sets related to the value of
lval
before
stmt
:
- the forward selection,
- the both way selection,
- the backward selection.
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)
Pervasives.ref
compute the set of statements where the given annotation has the same
value than it has before the given stmt.
Also return the
val check_asserts : (unit -> Cil_types.code_annotation list) Pervasives.ref
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) Pervasives.ref
Same analysis than check_asserts
but change assert to remove by true
val get_defs : (Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
(Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option)
Pervasives.ref
Returns the set of statements that define lval
before stmt
in kf
.
Also returns the zone that is possibly not defined.
Can return None
when the information is not available (Pdg missing).
val get_defs_with_type : (Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option)
Pervasives.ref
Returns a map from the statements that define lval
before stmt
in
kf
. The first boolean indicates the possibility of a direct
modification at this statement, ie. lval = ...
or lval = f()
.
The second boolean indicates a possible indirect modification through
a call.
Also returns the zone that is possibly not defined.
Can return None
when the information is not available (Pdg missing).
Zones
type
t_zones = Locations.Zone.t Cil_datatype.Stmt.Hashtbl.t
val build_zones : (Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval -> Cil_datatype.Stmt.Hptset.t * t_zones)
Pervasives.ref
val pretty_zones : (Format.formatter -> t_zones -> unit) Pervasives.ref
val get_zones : (t_zones -> Cil_types.stmt -> Locations.Zone.t) Pervasives.ref