From 76e4240f6e17ab1f17200c603cf827b2bb28458d Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Fri, 13 Oct 2017 15:26:05 +0100
Subject: add blockaddress and indirectbr instructions

---
 lib/Core/ExecutorUtil.cpp | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib/Core/ExecutorUtil.cpp')

diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 62d65c31..a0f4de3d 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -119,6 +119,11 @@ namespace klee {
         assert(isa<ConstantExpr>(res) &&
                "result of constant vector built is not a constant");
         return cast<ConstantExpr>(res);
+      } else if (const BlockAddress * ba = dyn_cast<BlockAddress>(c)) {
+        // return the address of the specified basic block in the specified function
+        const auto arg_bb = (BasicBlock *) ba->getOperand(1);
+        const auto res = Expr::createPointer((uint64_t) (unsigned long) (void *) arg_bb);
+        return cast<ConstantExpr>(res);
       } else {
         std::string msg("Cannot handle constant ");
         llvm::raw_string_ostream os(msg);
-- 
cgit 1.4.1