Expand description
The read/write set analysis is a compositional analysis that starts from the leaves of the call graph and analyzes each procedure once. The result is a summary of the abstract paths read/written by each procedure and the value(s) returned by the procedure.
When the analysis encounters a call, it fetches the summary for the callee and applies it to the
current state. This logic (implemented in apply_summary) is by far the most complex part of themove
analysis.
Structs
A record of the glocals and locals accessed by the current procedure + the address values stored by locals or globals
A abstract ReadWriteSetState that has been (fully or partially) concretized by substituting
concrete values. Represented as a separate type to avoid confusion/comparison with an
overapproximate ReadWriteSet
Functions
Return a string representation of the summary for target