From 5a11142d2258c3fd6d2f394f652950545b155bcf Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 19 Nov 2018 18:41:02 +0000
Subject: [PATCH] Add a definition of alloca

Benchmarks not including headers files fail as we only provided a definition of
__builtin_alloca, which alloca expands to in standard libary headers, but none
for alloca directly.
---
 src/ansi-c/library/stdlib.c | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 7f72651a18f..b96b12a2239 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -147,6 +147,18 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   return res;
 }
 
+/* FUNCTION: alloca */
+
+#undef alloca
+
+void *__builtin_alloca(__CPROVER_size_t alloca_size);
+
+inline void *alloca(__CPROVER_size_t alloca_size)
+{
+__CPROVER_HIDE:;
+  return __builtin_alloca(alloca_size);
+}
+
 /* FUNCTION: free */
 
 #undef free