Merge pull request #671 from smackers/optimize-galloc

Do not generate calls to $galloc procedures for functions
smackers · Dec 22, 2020 · 2552c01 · 2552c01
2 parents 45ff4d7 + e1f2339
commit 2552c01
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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;
 }