analyzer
analyzer copied to clipboard
Unsoundness for Updates to Locals of Recursive Functions Reachable via Globals
@jerhard and I discovered an issue where we currently are unsound as we do not correctly account for some modifications via globals:
#include<stdlib.h>
#include<goblint.h>
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); // 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();
}
This implies that the valid-deref
checks for this probably also need to be reconsidered.
We should have a look at this some time after SV-COMP.