Merge pull request #1103 from romainbrenguier/bugfix/declare-pointer-before-use

Declare malloc-site symbols before they are used

Author: romainbrenguier

regression/strings-smoke-tests/java_object_allocation/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--refine-strings --show-goto-functions
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+char \([*]malloc_site.[0-9]*\)\[INFINITY\(\)\];\n\s*//.*\n\s*malloc_site.[0-9]*\s*=\s*MALLOC\(char \[INFINITY\(\)\], 2ull? \* INFINITY\(\)\);\n\s*//.*\n\s*cprover_string_array.[0-9]*\s*=\s*malloc_site.\d*;
+--

regression/strings-smoke-tests/java_object_allocation/test.desc

@@ -0,0 +1,9 @@
+public class test
+{
+   public static void check()
+   {
+      String s = new String("foo");
+      String t = new String("bar");
+      String u = s.concat(t);
+   }
+}

regression/strings-smoke-tests/java_object_allocation/test.java

@@ -224,12 +224,13 @@ exprt allocate_dynamic_object_with_decl(
 {
   std::vector<const symbolt *> symbols_created;
 
+  code_blockt tmp_block;
   exprt result=allocate_dynamic_object(
     target_expr,
     allocate_type,
     symbol_table,
     loc,
-    output_code,
+    tmp_block,
     symbols_created,
     cast_needed);
 
@@ -242,6 +243,9 @@ exprt allocate_dynamic_object_with_decl(
     output_code.add(decl);
   }
 
+  for(const exprt &code : tmp_block.operands())
+    output_code.add(to_code(code));
+
   return result;
 }