Merge pull request #3224 from JohnDumbell/jd/bugfix/temp_variable_type_wrong

Temporary stack variable being stored as the wrong type

Author: smowton

jbmc/regression/jbmc/temp_stack_variable_packing/External.class

@@ -0,0 +1,5 @@
+public class External {
+    public void Accept(int... args) {
+
+    }
+}

jbmc/regression/jbmc/temp_stack_variable_packing/External.java

@@ -0,0 +1,12 @@
+public class Primary {
+    private External ex = new External();
+
+    public void Run() {
+        this.ex.Accept(new int[]{0, 1, 2});
+        assert(false);
+    }
+
+    public void main() {
+        this.Run();
+    }
+}

jbmc/regression/jbmc/temp_stack_variable_packing/Primary.class

@@ -0,0 +1,7 @@
+CORE
+Primary.class
+--function Primary.main
+^\[java::Primary.Run:\(\)V\.assertion\.1\] assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

jbmc/regression/jbmc/temp_stack_variable_packing/Primary.java

@@ -3237,7 +3237,8 @@ void java_bytecode_convert_methodt::save_stack_entries(
     }
     if(replace)
     {
-      create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+      create_stack_tmp_var(
+          tmp_var_prefix, stack_entry.type(), block, stack_entry);
     }
   }
 }