analyzer
analyzer copied to clipboard
`var_eq` doesn't remove unreachable variables in `enter`
Here's enter for var_eq analysis:
https://github.com/goblint/analyzer/blob/5614dd34bb45e3bb7f960bfddd512d00106aa4aa/src/analyses/varEq.ml#L412-L430
The comment claims it tries to remove unreachable variables but nowhere does it actually do that.
This means that the analysis keeps around equalities from the entire call stack, which makes them large (and thus less efficient to manipulate). It also means more unnecessary contexts for the called function because it can in no way observe those variables. Finally, in my unassume benchmarking and tracing, I've noticed it can cause extra widening iterations in the called function due to equations on unreachable variables being invalidated.
Example
// PARAM: ---set ana.activated[+] "'var_eq'"
void foo() {
// var_eq has x == y here
}
int main() {
int x;
int y;
y = x;
foo();
return 0;
}