From b585a94ad0cb30570cf4f14e2dc1ebb43f694bb3 Mon Sep 17 00:00:00 2001
From: Julian Büning <julian.buening@rwth-aachen.de>
Date: Tue, 24 Jul 2018 22:04:02 +0200
Subject: add declarations to escapingFunctions

---
 lib/Module/KModule.cpp           | 11 ++++++++++-
 test/Feature/EscapingFunctions.c | 13 ++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index d185f687..07ad2229 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -275,9 +275,13 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
   infos = std::unique_ptr<InstructionInfoTable>(
       new InstructionInfoTable(module.get()));
 
+  std::vector<Function *> declarations;
+
   for (auto &Function : *module) {
-    if (Function.isDeclaration())
+    if (Function.isDeclaration()) {
+      declarations.push_back(&Function);
       continue;
+    }
 
     auto kf = std::unique_ptr<KFunction>(new KFunction(&Function, this));
 
@@ -297,6 +301,11 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
       escapingFunctions.insert(kf->function);
   }
 
+  for (auto &declaration : declarations) {
+    if (functionEscapes(declaration))
+      escapingFunctions.insert(declaration);
+  }
+
   if (DebugPrintEscapingFunctions && !escapingFunctions.empty()) {
     llvm::errs() << "KLEE: escaping functions: [";
     for (auto &Function : escapingFunctions)
diff --git a/test/Feature/EscapingFunctions.c b/test/Feature/EscapingFunctions.c
index 8c9612a5..bb9b8a4a 100644
--- a/test/Feature/EscapingFunctions.c
+++ b/test/Feature/EscapingFunctions.c
@@ -3,6 +3,8 @@
 // RUN: %klee -debug-print-escaping-functions --output-dir=%t.klee-out %t.bc 2> %t.log
 // RUN: FileCheck --input-file=%t.log %s
 
+#include <stdint.h>
+
 int functionpointer(void) {
     return 1;
 }
@@ -33,6 +35,9 @@ two:
     return 2;
 }
 
+int function_declaration(void);
+uint8_t bitcasted_function_declaration(void);
+
 int main(int argc, char *argv[]) {
     int (*f1)(void) = functionpointer;
     f1();
@@ -44,6 +49,12 @@ int main(int argc, char *argv[]) {
 
     blockaddress(argc);
 
-    // CHECK: KLEE: escaping functions: {{\[((functionpointer|functionpointer_as_argument|bitcasted_functionpointer), ){3}\]}}
+    int (*f3)(void) = function_declaration;
+    f3();
+
+    uint64_t (*f4)(void) =(uint64_t (*)(void))bitcasted_function_declaration;
+    f4();
+
+    // CHECK: KLEE: escaping functions: {{\[((functionpointer|functionpointer_as_argument|bitcasted_functionpointer|function_declaration|bitcasted_function_declaration), ){5}\]}}
     return 0;
 }
-- 
cgit 1.4.1