8 files changed, 0 insertions, 103 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 69b29865..711cf1b3 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -144,8 +144,6 @@ public:
   std::set<std::string> arrayNames;
 
   std::string getFnAlias(std::string fn);
-  void addFnAlias(std::string old_fn, std::string new_fn);
-  void removeFnAlias(std::string fn);
 
   // The objects handling the klee_open_merge calls this state ran through
   std::vector<ref<MergeHandler> > openMergeStack;
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 9dcc9f5f..2446fc07 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -138,14 +138,6 @@ extern "C" {
   /* Enable/disable forking. */
   void klee_set_forking(unsigned enable);
 
-  /* klee_alias_function("foo", "bar") will replace, at runtime (on
-     the current path and all paths spawned on the current path), all
-     calls to foo() by calls to bar().  foo() and bar() have to exist
-     and have identical types.  Use klee_alias_function("foo", "foo")
-     to undo.  Be aware that some special functions, such as exit(),
-     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);
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 70d5d21c..48154383 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -173,14 +173,6 @@ std::string ExecutionState::getFnAlias(std::string fn) {
   else return "";
 }
 
-void ExecutionState::addFnAlias(std::string old_fn, std::string new_fn) {
-  fnAliases[old_fn] = new_fn;
-}
-
-void ExecutionState::removeFnAlias(std::string fn) {
-  fnAliases.erase(fn);
-}
-
 /**/
 
 llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm) {
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index e18d3534..231bd88d 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -108,7 +108,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_stack_trace", handleStackTrace, false),
   add("klee_warning", handleWarning, false),
   add("klee_warning_once", handleWarningOnce, false),
-  add("klee_alias_function", handleAliasFunction, false),
   add("malloc", handleMalloc, true),
   add("memalign", handleMemalign, true),
   add("realloc", handleRealloc, true),
@@ -299,20 +298,6 @@ void SpecialFunctionHandler::handleSilentExit(ExecutionState &state,
   executor.terminateState(state);
 }
 
-void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
-						 KInstruction *target,
-						 std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==2 && 
-         "invalid number of arguments to klee_alias_function");
-  std::string old_fn = readStringAtAddress(state, arguments[0]);
-  std::string new_fn = readStringAtAddress(state, arguments[1]);
-  KLEE_DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn
-                                           << "() with " << new_fn << "()\n");
-  if (old_fn == new_fn)
-    state.removeFnAlias(old_fn);
-  else state.addFnAlias(old_fn, new_fn);
-}
-
 void SpecialFunctionHandler::handleAssert(ExecutionState &state,
                                           KInstruction *target,
                                           std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index fdb6b6de..e041a3e4 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -111,7 +111,6 @@ namespace klee {
     HANDLER(handleDeleteArray);
     HANDLER(handleExit);
     HANDLER(handleErrnoLocation);
-    HANDLER(handleAliasFunction);
     HANDLER(handleFree);
     HANDLER(handleGetErrno);
     HANDLER(handleGetObjSize);
diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c
deleted file mode 100644
index 6a5e9174..00000000
--- a/test/Feature/AliasFunction.c
+++ /dev/null
@@ -1,37 +0,0 @@
-// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
-// RUN: grep -c foo %t1.log | grep 5
-// RUN: grep -c bar %t1.log | grep 4
-
-#include <stdio.h>
-#include <stdlib.h>
-
-void __attribute__ ((noinline)) foo() { printf("  foo()\n"); }
-void __attribute__ ((noinline)) bar() { printf("  bar()\n"); }
-
-int main() {
-  int x;
-  klee_make_symbolic(&x, sizeof(x), "x");
-
-  // call once, so that it is not removed by optimizations
-  bar();
-
-  // no aliases
-  foo();
-
-  if (x > 10)
-  {
-    // foo -> bar
-    klee_alias_function("foo", "bar");
-
-    if (x > 20)
-      foo();
-  }
-  
-  foo();
-
-  // undo
-  klee_alias_function("foo", "foo");
-  foo();
-}
diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c
deleted file mode 100644
index 1f863de1..00000000
--- a/test/Feature/AliasFunctionExit.c
+++ /dev/null
@@ -1,31 +0,0 @@
-// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
-// RUN: grep -c START %t1.log | grep 1
-// RUN: grep -c END %t1.log | grep 2
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <unistd.h>
-
-void start(int x) {
-  printf("START\n");
-  if (x == 53)
-    exit(1);
-}
-
-void __attribute__ ((noinline)) end(int status) {
-  klee_alias_function("exit", "exit");
-  printf("END: status = %d\n", status);
-  exit(status);
-}
-
-
-int main() {
-  int x;
-  klee_make_symbolic(&x, sizeof(x), "x");
-
-  klee_alias_function("exit", "end");
-  start(x);
-  end(0);
-}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index be90548e..99a9bf2a 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -780,7 +780,6 @@ static const char *modelledExternals[] = {
   "klee_silent_exit",
   "klee_warning",
   "klee_warning_once",
-  "klee_alias_function",
   "klee_stack_trace",
   "llvm.dbg.declare",
   "llvm.dbg.value",