Module Writes

module Writes: sig .. end

Computations of the statements that write a given memory zone.

Find the statements that writes a given zone. This is a lightweight version of module Scope.Defs. Instead of using PDGs (that may be very costly to compute), we only use Inout. This also means that we can find effects after* the stmt the user has chosen.

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.