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 as before the given stmt. Also returns the eventual code annotations
that are implied by the one given as argument.
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 mark the assertions as proven.
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