karelklic / canal

Abstract interpreter for real-world application programs
https://github.com/karelklic/canal/wiki
Other
32 stars 2 forks source link

Increase precision of basic store operation #105

Closed karelklic closed 11 years ago

karelklic commented 11 years ago

When a pointer points to a single memory target, storing a value should rewrite the old value instead of merging with it.

int a = 0, b = 1, c = 2;
int *ptr = &a;
if (a)
  l1:  ptr = &b;
else
  l2:  ptr = &c;

l3: *ptr = 0;
Iteration order worst case:
just l3: 0 stored nowhere, ptr has no targets
just l1 l3: 0 stored to b, b is {0}
l1 l2 l3: 0 merged to b and c, b is {0,1}, c is {0,2}