From af8447a670de1957d89e5a08cd59f3446e3a67de Mon Sep 17 00:00:00 2001
From: Martin Nowack <martin.nowack@gmail.com>
Date: Tue, 13 Aug 2013 16:35:14 +0200
Subject: Handle additional debug intrinsics of LLVM

---
 tools/klee/main.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 0c485571..b5a063a4 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -715,7 +715,11 @@ static const char *modelledExternals[] = {
   "klee_warning_once", 
   "klee_alias_function",
   "klee_stack_trace",
-  "llvm.dbg.stoppoint", 
+  "llvm.dbg.stoppoint",
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
+  "llvm.dbg.declare",
+  "llvm.dbg.value",
+#endif
   "llvm.va_start", 
   "llvm.va_end", 
   "malloc", 
-- 
cgit 1.4.1