Handle the LLVM exception system in Why3 generation #2
Description
LLVM has instructions made for exception handling, which are used by compilers such as clang++. However, we currently are not able to model these instructions in WhyR. To support all of LLVM, exceptions will have to be modeled.
This is difficult for various reasons:
- It requires non-local branching in some cases
- Exception handling is scoped dynamically
- The inputs to catch blocks are decided by "personality functions" in LLVM, which are essentially black boxes