Check for null this-argument at virtual callsites

Author: smowton

regression/cbmc-java/NondetArray2/NondetArray2.class

@@ -8,6 +8,8 @@ void main()
 
     int num = 0;
     for (Integer i : ints) {
+      if(i == null)
+        continue;
       num *= i.intValue();
     }
     assert num == 0;

regression/cbmc-java/NondetArray2/NondetArray2.java

@@ -9,6 +9,8 @@ void main()
 
     int num = 0;
     for (Integer i : ints) {
+      if(i == null)
+        continue;
       num *= i.intValue();
     }
     assert num == 0;

regression/cbmc-java/NondetArray3/NondetArray3.class

@@ -5,7 +5,7 @@ public class test
 {
   public static void main(C c)
   {
-    if(c==null)
+    if(c==null || c.a==null)
       return;
     c.a.f();
   }

regression/cbmc-java/NondetArray3/NondetArray3.java

@@ -453,6 +453,19 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)
     add_expr_instrumentation(block, code_function_call.lhs());
     add_expr_instrumentation(block, code_function_call.function());
 
+    const code_typet &function_type=
+      to_code_type(code_function_call.function().type());
+
+    // Check for a null this-argument of a virtual call:
+    if(function_type.has_this())
+    {
+      block.copy_to_operands(
+        check_null_dereference(
+          code_function_call.arguments()[0],
+          code_function_call.source_location(),
+          true));
+    }
+
     for(const auto &arg : code_function_call.arguments())
       add_expr_instrumentation(block, arg);