Changes between Version 5 and Version 6 of MemoryAnalysis

Timestamp:

03/08/16 13:10:05 (10 years ago)

Author:

zmanchun

Comment:

--

MemoryAnalysis

@@ -13 +13 @@
 === Impact memory unit analysis ===
 The analysis below is an over approximation.
+
+Given a location `L`, which has outgoing statements `s1, s2, ... sn`, the impact memory units of `L` is:\\
+`impact(L) = impact(s1) U impact(s2) U ... U impact(sn)`.
+
+Reachable memory units analysis:
+
+`reach(L) = U` ,,`L --> L'`,, `reach(L') U impact(L)`.
+
 ==== 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`.
@@ -86 +94 @@
    **TBC**
  * otherwise:\\
-   `impact(l := f(e0, e1, e2, ...)) = impact(l) U impact(e0) U impact(e1) ...`
+   `impact(l := f(e0, e1, e2, ...)) = impact(l) U impact(e0) U impact(e1) ... U impact(f)`, where `impact(f)` is the impact memory unit set of the function `f`.
 
 3. guarded statement: `[e]s`
@@ -96 +104 @@
 
 
-