module Writes:sig
..end
type
effects = {
|
direct : |
(* |
Direct affectation
lv = ... , or modification through
a call to a leaf function. | *) |
|
indirect : |
(* |
Modification inside the body of called function
f(...) | *) |
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.