Frama-C:
Plug-ins:
Libraries:

Frama-C API - Writes

type t =
  1. | Assign of Frama_c_kernel.Cil_types.stmt
    (*

    Direct assignment.

    *)
  2. | CallDirect of Frama_c_kernel.Cil_types.stmt
    (*

    Modification by a called leaf function.

    *)
  3. | CallIndirect of Frama_c_kernel.Cil_types.stmt
    (*

    Modification inside the body of a called function.

    *)
  4. | GlobalInit of Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.initinfo
    (*

    Initialization of a global variable.

    *)
  5. | 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.