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.