diff --git a/tests/regression/01-cpa/75-update-local-via-global.c b/tests/regression/01-cpa/75-update-local-via-global.c new file mode 100644 index 00000000000..f57fe11242b --- /dev/null +++ b/tests/regression/01-cpa/75-update-local-via-global.c @@ -0,0 +1,31 @@ +#include +#include +int g; +int* global = &g; + +void fun() { + int top; + int top2; + int x; + + if(top) { + global = &x; + } + + x = 8; + if(top2) { + fun(); + } + __goblint_check(x == 8); // UNKNOWN! We claim this holds, but it most not really hold: If top is false in the callee, it updates x to `5` + + // May dereference x of previous invocation, should probably warn + *global = 5; +} + +int main() { + fun(); + + *global = 8; //We should probably warn here for invalid deref (?) + + fun(); +} \ No newline at end of file