Do not generate calls to $galloc procedures for functions

smackers · Dec 21, 2020 · e1f2339 · e1f2339
1 parent 45ff4d7
commit e1f2339
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;
 }