Merge pull request #4997 from thomasspriggs/tas/java_constructor_fix

 Fix the `this` argument used when checking a constructor

Author: thomasspriggs

jbmc/regression/jbmc/constructor2/Constructor2.class

@@ -0,0 +1,5 @@
+class Constructor2 {
+  int myField;
+
+  Constructor2() { assert myField == 0; }
+}

jbmc/regression/jbmc/constructor2/Constructor2.java

@@ -0,0 +1,11 @@
+CORE
+Constructor2.class
+--function 'Constructor2.<init>'
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Test that a field of a class being constructed is zero initialised before the
+constructor is called, where the function being checked is a constructor.

jbmc/regression/jbmc/constructor2/test.desc

@@ -297,8 +297,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &message_handler)
 {
-  const java_method_typet::parameterst &parameters =
-    to_java_method_type(function.type).parameters();
+  const java_method_typet &function_type = to_java_method_type(function.type);
+  const java_method_typet::parameterst &parameters = function_type.parameters();
 
   code_blockt init_code;
   exprt::operandst main_arguments;
@@ -324,6 +324,22 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
     // be null
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
+    if(is_this && function_type.get_is_constructor())
+    {
+      const symbol_exprt result = fresh_java_symbol(
+                                    p.type(),
+                                    "this_parameter",
+                                    function.location,
+                                    function.name,
+                                    symbol_table)
+                                    .symbol_expr();
+      main_arguments[param_number] = result;
+      init_code.add(code_declt{result});
+      init_code.add(
+        code_assignt{result, side_effect_exprt(ID_java_new, p.type())});
+      continue;
+    }
+
     java_object_factory_parameterst factory_parameters =
       object_factory_parameters;
     // only pointer must be non-null