From e1f2339d2e1904ab6a5c0863d602e5b41fd07681 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Mon, 21 Dec 2020 15:36:26 -0700
Subject: [PATCH] Do not generate calls to $galloc procedures for functions

---
 lib/smack/SmackRep.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 998966787..451ee725c 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -1305,7 +1305,9 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v) {
     decls.push_back(Decl::axiom(Expr::eq(
         Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding)))));
   }
-  globalAllocations[v] = size;
+
+  if (!llvm::isa<Function>(v))
+    globalAllocations[v] = size;
 
   return decls;
 }