Optimize the control flow graph to reduce false positives

[arthaud]

The analyzer generates false positives when the code uses the following pattern:

#include <ikos/analyzer/intrinsic.h>
#define SUCCESS 0

extern int f(void);
extern int g(void);
extern int h(void);

int x = 0;

int main() {
    int status = f();
    if (status == SUCCESS) {
        status = g();
        x = 1;
    }
    if (status == SUCCESS) {
        status = h();
        __ikos_assert(x == 1);
    }
    return 0;
}

The analyzer generates the following warning:

test.c:18:9: warning: assertion could not be proven
        __ikos_assert(x == 1);
        ^

First, this code pattern is questionable and I would recommend not using it. It is hard to read and causes trouble to static analyzers. Prefer the early-return pattern, see this example.

Anyway, we could solve this false positive by optimizing the control flow graph. The current control flow graph is here. We could write an optimization pass that replaces the edge from #3 to #4 by an edge from #3 to #6. This would fix remove the warning.