Module Studia.Writes

module Writes: sig .. end

type effects = {
   direct : bool; (*

Direct affectation lv = ..., or modification through a call to a leaf function.

*)
   indirect : bool; (*

Modification inside the body of called function f(...)

*)
}

Given an effect e, something is directly modified by e (through an affectation, or through a call to a leaf function) if direct holds, and indirectly (through the effects of a call) otherwise.

val compute : Locations.Zone.t -> (Cil_types.stmt * effects) list

compute z finds all the statements that modifies z, and for each statement, indicates whether the modification is direct or indirect.