== 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`.
let`mu(e)` be a function to convert an expression, of pointer type or being a left-hand-side expression, to a memory unit.

1. abstract function call: `f(e0,e1, ...)`
    `impact(f(e0,e1, ...)) = impact(e0) U impact(e1) ...`
2. address-of: `&le`
    `impact($le)=impact(sub(le))`
3. array literal: `{e0, e1, ...}`
    `impact({e0, e1, ...}) = impact(e0) U impact(e1) ...`
4. binary expression: `e0 op e1`
    `impact(e0 op e1) = impact(e0) U impact(e1)`
5. bound variable expression: `eb` 
    `impact(eb)=\empty`
6. cast expression: `(T)e`
    `impact((T)e)=impact(e)`
7. char literal: `{e0, e1, ...}`
    similar to array literal
8. conditional expression: `e0 ? e1 : e2`
    `impact(e0 ? e1 : e2) = impact(e0) U impact(e1) U impact(e2)`
9. dereference expression: `*e`
    `impact(*e) = mu(e) U impact(sub(e))`
    the impact memory units of `*e` include the memory unit refers to by `e`, and the impact memory units of the sub-expressions of `e`.
    e.g., the impact memory units of `*(p+i)` is `{mu(p+5), impact(i)}`, because `p` is of pointer type and `sub(p+i)` is `{i}`.
10. derivative call expression: `de`
      `impact(de) = \empty`
11. domain guard expression: `(int i0, i1, ... : e)`
      `impact((int i0, i1, ... : e)) = impact(e)`
12. dot expression: `e.k`
      `impact(e.k) = mu(e.k) U impact(sub(e))`
       the impact memory units of `e.k` include the memory unit refers to by `e`, and the impact memory units of the sub-expressions of `e`.
       e.g., the impact memory units of `points[k].x` is `{mu(points[k]+x), impact(k)}`, because `sub(points[k])` is `{k}`.
13. quantified expression: `quantifier er: e` where `er` is the restriction expression
      `impact(quantifier er: e) = impact(er) U impact(e)`
14. rectangular domain expression: `{e0, e1, ...}`
      similar to array literal
15. regular range expression: `{el, eh#es}`
      `impact({el, eh#es}) = impact(el) U impact(eh) U impact(es)`
16. scope-of expression: `scopeof(e)`
      `impact(scopeof(e))=\empty`
17. sizeof expression: `sizeof(e)`
      `impact(sizeof(e))=\empty`
18. struct or union literal: `{e0, e1, ...}`
      similar to array literal
19. subscript expression: `ea[ei]`
      `impact(ea[ei])=mu(ea[ei]) U impact(sub(ea)) U impact(ei)`
       for example, the impact units of `(a[i])[j]` is `mu(a[i][j]) U impact(i) U impact(j)` because `sub(a[i])` is `{i}`.

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

1. abstract function call: `f(e0,e1, ...)`
    `sub(f(e0,e1, ...)) = {e0, e1, ...}`
2. address-of: `&le`
    `sub(&le)={le} U sub(le)`
3. array literal: `{e0, e1, ...}`
    `sub({e0, e1, ...}) = {e0, e1, ...}``
 4. binary expression: `e0 op e1`
    `sub(e0 op e1) = e0.type== pointer ? {e1} : {e0, e1}`
5. bound variable expression: `eb` 
    `sub(eb)=\empty`
6. cast expression: `(T)e`
    `sub((T)e)={e}`

==== statements ====

1. assignment: `l := e`
   `impact(l := e) = impact(l) U impact(e)`;

2. call: `l := f(e0, e1, e2, ...)`
 * f is atomic specified (`$atomic_f`) and f has contracts: \\
   **TBC**
 * otherwise:\\
   `impact(l := f(e0, e1, e2, ...)) = impact(l) U impact(e0) U impact(e1) ...`

3. guarded statement: `[e]s`
    `impact([e]s) = impact(e) U impact(s)`