Studia.Writes
type effects = {
direct : bool; | (* Direct affectation |
indirect : bool; | (* 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 :
Frama_c_kernel.Locations.Zone.t ->
(Frama_c_kernel.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.