From 2c8901f4fb9e61fa71d707311f4758147c4039ce Mon Sep 17 00:00:00 2001 From: Charlotte Brandt Date: Thu, 19 Dec 2024 10:19:33 +0100 Subject: [PATCH] added test from lin2vareq to affeq that found mistake in dim_add --- tests/regression/63-affeq/21-function_call.c | 21 ++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/regression/63-affeq/21-function_call.c diff --git a/tests/regression/63-affeq/21-function_call.c b/tests/regression/63-affeq/21-function_call.c new file mode 100644 index 0000000000..723b75e14a --- /dev/null +++ b/tests/regression/63-affeq/21-function_call.c @@ -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 + +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; +}