Unsound exception propagation analysis for functions never returning

[arthaud]

On the following code:

#include <stdio.h>
#include <ikos/analyzer/intrinsic.h>

int f() {
  throw "exception";
}

void g() {
  while(1) {
    f();
  }
}

int main() {
  try {
    g();
  } catch(...) {
    printf("exception caught\n");
  }
  return 0;
}

IKOS produces the following output:

test.cpp:18:5: unreachable: code is dead
    printf("exception caught\n");
    ^

IKOS is unsound because it thinks the catch block is unreachable. This is because the control flow graph of g doesn't have an exit block, see _Z1gv.pdf. The current design of the exception propagation analysis requires that all exit nodes are merged into one block, so that we can capture all the exceptions and propagate it to the caller.

We should investigate if LLVM could generate an invoke instead of a call and add a basic block that explicitly propagates the exception.