== Memory Analysis ==

=== Definitions ===
1. memory unit: `mu = (dyscopeID, variableID, reference, access)`
   A memory unit `mu` is referring to a certain region of a variable, which is defined by a dyscopeID and a variable ID. A `mu` has an access attribute which denotes whether the it is writable by a given process.

2. impact memory unit: a memory unit being accessed at the current location by a given process.

3. reachable impact memory unit: a memory unit being accessed at the current location or any reachable future location of a given process.

4. variable addressed-of: a variable that's used as the operand of the address-of operator `&`.

=== Impact memory unit analysis ===
The analysis below is an over approximation.
==== Expressions ====
let `e` be an expression, let `le` be an left-hand-side expression, let `impact(e)` be the set of impact memory units of `e`.

1. abstract function call: `e = f(e0,e1, ...)`
    `impact(f(e0,e1, ...)) = impact(e0) U impact(e1) ...`
2. address-of: `e=&le`
    `impact($le)=impact(sub(le))`
3. 

==== Sub-expressions ====
let `e` be an expression, let `sub(e)` be the set of sub-expressions of `e`.

1. abstract function call: `e = f(e0,e1, ...)`
    `sub(f(e0,e1, ...)) = {e0, e1, ...}`
2. address-of: `e=&le`
    `sub(&le)=sub(le)`
3.