Studia.Writes
type t =
| Assign of Frama_c_kernel.Cil_types.stmt
Direct assignment.
*)| CallDirect of Frama_c_kernel.Cil_types.stmt
Modification by a called leaf function.
*)| CallIndirect of Frama_c_kernel.Cil_types.stmt
Modification inside the body of a called function.
*)| GlobalInit of Frama_c_kernel.Cil_types.varinfo
* Frama_c_kernel.Cil_types.initinfo
Initialization of a global variable.
*)| FormalInit of Frama_c_kernel.Cil_types.varinfo
* (Frama_c_kernel.Cil_types.kernel_function
* Frama_c_kernel.Cil_types.stmt list)
list
Initialization of a formal parameter, with a list of callsites.
*)val compute : Frama_c_kernel.Locations.Zone.t -> t list
compute z
finds all the statements that modifies z
, and for each statement, indicates whether the modification is direct or indirect.