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
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: