Skip to content

Commit

Permalink
#197, add example that summarizes one alleged reason why the heap sep…
Browse files Browse the repository at this point in the history
…arator does not separate well, currently
  • Loading branch information
alexandernutz committed Jan 9, 2018
1 parent 2dedfb1 commit 87f1479
Showing 1 changed file with 28 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
/**
* Currently (09.01.2018), the heap separator cannot separate the memory array
* in this example, although there is a semantics-preserving separation.
* (partition would be {{p}, {q,r}})
* Combination of triggers for this problem:
* - r is used to access the memory array, thus it is taken into account for
* partitioning.
* - r has a nondeterministic value at the positions where p and q are
* dereferenced, it dangles between the potential partition blocks so to say,
* and thus triggers their unification.
*/
int * nondet() {
int *i;
return i;
}

int main() {

int *p = malloc(sizeof(int));
int *q = malloc(sizeof(int));

int *r = q;
int z = *r;
r = nondet();

int x = *p;
int y = *q;
}

0 comments on commit 87f1479

Please sign in to comment.