From 2b0b0f89fcfff828b6dd8c20f58d872c7395dba4 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Fri, 2 Aug 2019 16:54:57 +0100
Subject: Executor: fix missing default case in switch instruction
---
lib/Core/Executor.cpp | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
(limited to 'lib/Core')
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 655d6005..4ff181f5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1795,10 +1795,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
// Handle possible different branch targets
// We have the following assumptions:
- // - each case value is mutual exclusive to all other values including the
- // default value
+ // - each case value is mutual exclusive to all other values
// - order of case branches is based on the order of the expressions of
- // the scase values, still default is handled last
+ // the case values, still default is handled last
std::vector<BasicBlock *> bbOrder;
std::map<BasicBlock *, ref<Expr> > branchTargets;
@@ -1822,6 +1821,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
it != itE; ++it) {
ref<Expr> match = EqExpr::create(cond, it->first);
+ // skip if case has same successor basic block as default case
+ // (should work even with phi nodes as a switch is a single terminating instruction)
+ if (it->second == si->getDefaultDest()) continue;
+
// Make sure that the default value does not contain this target's value
defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match));
--
cgit 1.4.1