diff --git a/tests/regression/77-lin2vareq/14-join_after_guard.c b/tests/regression/77-lin2vareq/14-join_after_guard.c new file mode 100644 index 0000000000..73d13384f3 --- /dev/null +++ b/tests/regression/77-lin2vareq/14-join_after_guard.c @@ -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; +} diff --git a/tests/regression/77-lin2vareq/15-join-non-constant.c b/tests/regression/77-lin2vareq/15-join-non-constant.c new file mode 100644 index 0000000000..16b1ccd33e --- /dev/null +++ b/tests/regression/77-lin2vareq/15-join-non-constant.c @@ -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; +}