Skip to content

Commit

Permalink
Added two test cases for join
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Jan 4, 2024
1 parent f872e55 commit 46802dd
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 0 deletions.
17 changes: 17 additions & 0 deletions tests/regression/77-lin2vareq/14-join_after_guard.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//SKIP PARAM: --set ana.activated[+] lin2vareq --set ana.relation.privatization top --set sem.int.signed_overflow assume_none
// from 63-affeq/04-join-after-guard
int main(void) {
int zero = 0;
int x = 0;

int t, r, d;
if (t) {
r = 10;
d = 500;
} else {
r = 10;
}
__goblint_check(r == 10); //SUCCESS
__goblint_check(d == 500); //UNKNOWN!
return 0;
}
22 changes: 22 additions & 0 deletions tests/regression/77-lin2vareq/15-join-non-constant.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// SKIP PARAM: --set ana.activated[+] lin2vareq --set ana.relation.privatization top --set sem.int.signed_overflow assume_none

int main(void) {
int a, b, c, d;

int t;
if (t) {
b = a + 2;
c = a + 7;
d = a + 1;
} else {
b = a + 30;
c = a + 35;
d = a + 10;
}
__goblint_check(c == b + 5); // SUCCESS
__goblint_check(c == b + 3); // FAILURE
__goblint_check(d == b + 3); // UNKNOWN!
__goblint_check(b == a + 2); // UNKNOWN!

return 0;
}

0 comments on commit 46802dd

Please sign in to comment.