Merge pull request #4242 from tautschnig/allocate-fix

symex_allocate: only use alloc_size when set

Author: tautschnig

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;
+}

regression/cbmc/Malloc25/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;