Skip to content

Commit

Permalink
added test from lin2vareq to affeq that found mistake in dim_add
Browse files Browse the repository at this point in the history
  • Loading branch information
charlotte-brandt committed Dec 19, 2024
1 parent 92802e5 commit 2c8901f
Showing 1 changed file with 21 additions and 0 deletions.
21 changes: 21 additions & 0 deletions tests/regression/63-affeq/21-function_call.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none
// This test was added from 77-lin2vareq because it found mistakes in dim_add that weren't detected by the other tests
#include <goblint.h>

int check_equal(int x, int y, int z) {
__goblint_check(x == y);
__goblint_check(z == y);
__goblint_check(x == z);
return 8;
}

int main(void) {
int x, y, z;

y = x;
z = y;

check_equal(x, y, z);

return 0;
}

0 comments on commit 2c8901f

Please sign in to comment.