Module 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 compare : t -> t -> int
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.