LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:introduction_to_pointer_analysis [2008/05/21 10:40]
vkuncak
sav08:introduction_to_pointer_analysis [2008/05/21 10:42]
vkuncak
Line 48: Line 48:
   * Can compiler prove one branch is dead?  ​   * Can compiler prove one branch is dead?  ​
   * Can it do common subexpression elimination?​   * Can it do common subexpression elimination?​
-<​code ​c>+<​code>​
   x = sin(z);   x = sin(z);
   *p = 4.0;   *p = 4.0;
Line 58: Line 58:
  
 Is Is
-<​code ​c>+<​code>​
   int* p1, p2;   int* p1, p2;
   ...S...   ...S...
Line 65: Line 65:
 </​code>​ </​code>​
 equivalent to equivalent to
-<​code ​c>+ 
 +<​code>​
   int* p1, p2;   int* p1, p2;
   ...S...   ...S...
Line 73: Line 74:
  
 There are also corresponding examples in Java, ocaml. There are also corresponding examples in Java, ocaml.
-<​code ​java>+ 
 +<​code>​
   x.f = 3;   x.f = 3;
   p.f = 4;   p.f = 4;
Line 82: Line 84:
   }   }
 </​code>​ </​code>​
-<​code ​ocaml>+ 
 +<​code>​
   let x = ref 3 in   let x = ref 3 in
   let p = x in   let p = x in
Line 91: Line 94:
  
 How we can describe this semantically?​ (Recall verification condition generation in the presence of structures):​ we can view functions as arrays: How we can describe this semantically?​ (Recall verification condition generation in the presence of structures):​ we can view functions as arrays:
-<​code ​java>+ 
 +<​code>​
   f[x] = 3;   f[x] = 3;
   f[p] = 4;   f[p] = 4;
Line 114: Line 118:
  
   * **pointer analysis:** represent (usually disjoint) sets of locations to which each variable points to. For example, if we can determine that a pointer p points to an abstract location 1, and q points to location 2. If location 1 and location 2 are disjoint, then we can be sure that p and q do not overlap.  ​   * **pointer analysis:** represent (usually disjoint) sets of locations to which each variable points to. For example, if we can determine that a pointer p points to an abstract location 1, and q points to location 2. If location 1 and location 2 are disjoint, then we can be sure that p and q do not overlap.  ​
-  * **alias analysis:** can two symbolic expressions be an '​alias'​ for the same physical location i.e. can they point to the same location. ​+  * **alias analysis:** can two symbolic expressions be an '​alias'​ for the same physical location i.e. can they point to the same location.