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.


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)
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
val check_asserts : unit -> Cil_types.code_annotation list
val rm_asserts : unit -> unit
module R: Plugin.General_services 

for internal use

val get_lval_zones : for_writing:bool ->
Cil_types.stmt ->
Cil_types.lval -> Locations.Zone.t * bool * Locations.Zone.t