diff options
| author | Hui Peng <benquike@gmail.com> | 2019-11-01 18:10:10 -0400 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2019-11-04 21:31:16 +0000 |
| commit | be9b714c1cf617877b8bcb6e1d5e63c3b694075a (patch) | |
| tree | 00807a6b1b4939efa5e35951aee29aef3fcdba03 /lib/Core | |
| parent | 168d245b4ac4149b6fcc060a4add341334ade4b0 (diff) | |
| download | klee-be9b714c1cf617877b8bcb6e1d5e63c3b694075a.tar.gz | |
Remove the duplicated check for DebugInfoIntrinsic
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4ff181f5..bc889f25 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1913,10 +1913,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Value *fp = cs.getCalledValue(); Function *f = getTargetFunction(fp, state); - // Skip debug intrinsics, we can't evaluate their metadata arguments. - if (isa<DbgInfoIntrinsic>(i)) - break; - if (isa<InlineAsm>(fp)) { terminateStateOnExecError(state, "inline assembly is unsupported"); break; |