module Writes:sig
..end
type
effects = {
|
direct : |
(* | Direct affectation | *) |
|
indirect : |
(* | Modification inside the body of called function
| *) |
}
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.