diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-07-18 16:04:19 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-07-20 11:16:51 +0100 |
commit | ffe695c29915cf8605b2fb807cd083cdcc769d47 (patch) | |
tree | 43de93aa43ef870a28ff1edf0897b28f18afb1f3 /LICENSE.TXT | |
parent | 8e8732d482e42e363f0f4c51794ed966701371e7 (diff) | |
download | klee-ffe695c29915cf8605b2fb807cd083cdcc769d47.tar.gz |
Replace assertions of types on LLVM instructions in the Executor with a
pass that checks these assertions. This improves several things. * This pass provides more friendly messages than assertions in that it just emits a warning and carries on checking the rest of the instructions. * The takes the checks outside of the Executor's hot path and so avoids checking the same instruction multiple times. Now each instruction is only checked once just before execution starts. The disadvantage of this approach is the check for invariants we expect to hold have been pulled far away from where we expect them to hold. After discussion with @ccadar and @MartinNowack it was decided we will take this hit to readability for better performance and simpler code in the Executor.
Diffstat (limited to 'LICENSE.TXT')
0 files changed, 0 insertions, 0 deletions