Skip to content

Commit

Permalink
Add more intricate example (with TODO for refinement of both sides)
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed May 20, 2024
1 parent dc2a9c3 commit b7265e7
Showing 1 changed file with 27 additions and 0 deletions.
27 changes: 27 additions & 0 deletions tests/regression/27-inv_invariants/22-meet-ptrs.c
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,32 @@
#include <stdlib.h>
#include <time.h>

int more_intricate() {
int arr[20];

int top;

int i = 2;
int j = 8;
if(top) {
i = 8;
j = 9;
}

int* imprecise1 = &arr[i]; // &arr[2..8]
int* imprecise2 = &arr[j]; // &arr[8..9]

if(imprecise1 == imprecise2) {
__goblint_check(imprecise1 == &arr[8]);
__goblint_check(imprecise2 == &arr[8]); //TODO (Refinement should happen in both directions!)
}

if(imprecise1 == &arr[j]) {
__goblint_check(imprecise1 == &arr[8]);
}

}


int main() {
int arr[20];
Expand All @@ -20,5 +46,6 @@ int main() {
__goblint_check(imprecise == &arr[2]);
}

more_intricate();
return 0;
}

0 comments on commit b7265e7

Please sign in to comment.