1 files changed, 106 insertions, 0 deletions
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
new file mode 100644
index 00000000..d5d1af93
--- /dev/null
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -0,0 +1,106 @@
+//===-- SpecialFunctionHandler.h --------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_SPECIALFUNCTIONHANDLER_H
+#define KLEE_SPECIALFUNCTIONHANDLER_H
+
+#include <map>
+#include <vector>
+#include <string>
+
+namespace llvm {
+  class Function;
+}
+
+namespace klee {
+  class Executor;
+  class Expr;
+  class ExecutionState;
+  class KInstruction;
+  template<typename T> class ref;
+  
+  class SpecialFunctionHandler {
+  public:
+    typedef void (SpecialFunctionHandler::*Handler)(ExecutionState &state,
+                                                    KInstruction *target, 
+                                                    std::vector<ref<Expr> > 
+                                                      &arguments);
+    typedef std::map<const llvm::Function*, 
+                     std::pair<Handler,bool> > handlers_ty;
+
+    handlers_ty handlers;
+    class Executor &executor;
+
+  public:
+    SpecialFunctionHandler(Executor &_executor);
+
+    /// Perform any modifications on the LLVM module before it is
+    /// prepared for execution. At the moment this involves deleting
+    /// unused function bodies and marking intrinsics with appropriate
+    /// flags for use in optimizations.
+    void prepare();
+
+    /// Initialize the internal handler map after the module has been
+    /// prepared for execution.
+    void bind();
+
+    bool handle(ExecutionState &state, 
+                llvm::Function *f,
+                KInstruction *target,
+                std::vector< ref<Expr> > &arguments);
+
+    /* Convenience routines */
+
+    std::string readStringAtAddress(ExecutionState &state, ref<Expr> address);
+    
+    /* Handlers */
+
+#define HANDLER(name) void name(ExecutionState &state, \
+                                KInstruction *target, \
+                                std::vector< ref<Expr> > &arguments)
+    HANDLER(handleAbort);
+    HANDLER(handleAssert);
+    HANDLER(handleAssertFail);
+    HANDLER(handleAssume);
+    HANDLER(handleCalloc);
+    HANDLER(handleCheckMemoryAccess);
+    HANDLER(handleDefineFixedObject);
+    HANDLER(handleDelete);    
+    HANDLER(handleDeleteArray);
+    HANDLER(handleExit);
+    HANDLER(handleAliasFunction);
+    HANDLER(handleFree);
+    HANDLER(handleGetErrno);
+    HANDLER(handleGetObjSize);
+    HANDLER(handleGetValue);
+    HANDLER(handleIsSymbolic);
+    HANDLER(handleMakeSymbolic);
+    HANDLER(handleMalloc);
+    HANDLER(handleMallocN);
+    HANDLER(handleMarkGlobal);
+    HANDLER(handleMerge);
+    HANDLER(handleNew);
+    HANDLER(handleNewArray);
+    HANDLER(handlePreferCex);
+    HANDLER(handlePrintExpr);
+    HANDLER(handlePrintRange);
+    HANDLER(handleRange);
+    HANDLER(handleRealloc);
+    HANDLER(handleReportError);
+    HANDLER(handleRevirtObjects);
+    HANDLER(handleSetForking);
+    HANDLER(handleSilentExit);
+    HANDLER(handleUnderConstrained);
+    HANDLER(handleWarning);
+    HANDLER(handleWarningOnce);
+#undef HANDLER
+  };
+} // End klee namespace
+
+#endif