From b5c07f4f37f3de6a3d8764f6255f54bbcbf3a0f6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 21 Feb 2019 01:06:02 +0000
Subject: [PATCH] symex_allocate: only use alloc_size when set

When alloc_size isn't set but the other conditions in the earlier branch are not
satisfied we must not use alloc_size. Fall back to building an array of
characters instead.
---
 regression/cbmc/Malloc25/main.c            | 7 +++++++
 regression/cbmc/Malloc25/test.desc         | 8 ++++++++
 src/goto-symex/symex_builtin_functions.cpp | 2 +-
 3 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Malloc25/main.c
 create mode 100644 regression/cbmc/Malloc25/test.desc

diff --git a/regression/cbmc/Malloc25/main.c b/regression/cbmc/Malloc25/main.c
new file mode 100644
index 00000000000..e94a97528ba
--- /dev/null
+++ b/regression/cbmc/Malloc25/main.c
@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main(int argc, char *argv[])
+{
+  int *p = malloc((size_t)argc * (size_t)argc * sizeof(int));
+  return 0;
+}
diff --git a/regression/cbmc/Malloc25/test.desc b/regression/cbmc/Malloc25/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Malloc25/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index fcaeedbb2ed..02c51072899 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -102,7 +102,7 @@ void goto_symext::symex_allocate(
 
           object_type = array_typet(*tmp_type, s);
         }
-        else
+        else if(alloc_size.has_value())
         {
           if(*alloc_size == *elem_size)
             object_type = *tmp_type;