about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2013-08-13 16:35:14 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2013-08-14 22:23:24 +0200
commitaf8447a670de1957d89e5a08cd59f3446e3a67de (patch)
tree4636c54a126c0d127da9bf4a1257a243613d49c6
parent39616bca565f1d3f958dc7e0e071ac5dc64f5439 (diff)
downloadklee-af8447a670de1957d89e5a08cd59f3446e3a67de.tar.gz
Handle additional debug intrinsics of LLVM
-rw-r--r--tools/klee/main.cpp6
1 files changed, 5 insertions, 1 deletions
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",