Improve precision in invariant by delaying joins #458
Description
In the process of #419 and its option exp.structs.meet-condition I came across the following possibility for an easy improvement.
In invariant, we could, for each variable the pointer may point to, do the meet with the right hand side separately. If this yields \bot
everywhere, the branch is definitely dead.
(Alternatively, one could also improve the pointer here to only point to those things for which the condition may hold)
This probably doesn't matter too much, but I wanted to write it down somewhere, such that we can potentially go back to it.
// PARAM: --enable ana.int.interval
int main(void) {
int top;
int two = 2;
int four = 4;
int* ptr = &two;
if(top) {
ptr = &four;
}
int a = 0;
if(*ptr == 3) {
a = 1;
}
assert(a == 0);
}