4 files changed, 12 insertions, 0 deletions
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 3d2d1782..aa47ce22 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -127,6 +127,9 @@ extern "C" {
      may not always work. */
   void klee_alias_function(const char* fn_name, const char* new_fn_name);
 
+  /* Print stack trace. */
+  void klee_stack_trace(void);
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 1b96d5f1..d3a86aac 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -80,6 +80,7 @@ HandlerInfo handlerInfo[] = {
   add("klee_print_expr", handlePrintExpr, false),
   add("klee_print_range", handlePrintRange, false),
   add("klee_set_forking", handleSetForking, false),
+  add("klee_stack_trace", handleStackTrace, false),
   add("klee_warning", handleWarning, false),
   add("klee_warning_once", handleWarningOnce, false),
   add("klee_alias_function", handleAliasFunction, false),
@@ -428,6 +429,12 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
   }
 }
 
+void SpecialFunctionHandler::handleStackTrace(ExecutionState &state,
+                                              KInstruction *target,
+                                              std::vector<ref<Expr> > &arguments) {
+  state.dumpStack(std::cout);
+}
+
 void SpecialFunctionHandler::handleWarning(ExecutionState &state,
                                            KInstruction *target,
                                            std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 37792faf..e8c2eedf 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -95,6 +95,7 @@ namespace klee {
     HANDLER(handleRevirtObjects);
     HANDLER(handleSetForking);
     HANDLER(handleSilentExit);
+    HANDLER(handleStackTrace);
     HANDLER(handleUnderConstrained);
     HANDLER(handleWarning);
     HANDLER(handleWarningOnce);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 756ebb68..2b7310ec 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -686,6 +686,7 @@ static const char *modelledExternals[] = {
   "klee_warning", 
   "klee_warning_once", 
   "klee_alias_function",
+  "klee_stack_trace",
   "llvm.dbg.stoppoint", 
   "llvm.va_start", 
   "llvm.va_end",