Fix __builtin_alloca classification

goblint · Sep 29, 2023 · 4090e74 · 4090e74
1 parent 5cca543
commit 4090e74
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -440,7 +440,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);
-    ("__builtin_alloca", special [__ "size" []] @@ fun size -> Malloc size);
+    ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size);
   ]
 
 let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[