Studia.Reads
Computations of the statements that read a given memory zone.
type t =
| Direct of Frama_c_kernel.Cil_types.stmt
Direct read by a statement.
*)| Indirect of Frama_c_kernel.Cil_types.stmt
Indirect read through a function call.
*)val compute : Frama_c_kernel.Locations.Zone.t -> t list
compute z
finds all the statements that read z
. The effects
information indicates whether the read occur on the given statement, or through an inner call for Call
instructions.