Merge pull request #960 from pkesseli/bugfix/main-and-args-not-internal

Avoid marking main function call / arguments as internal

Author: smowton

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class

@@ -0,0 +1,5 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Item {
+  public int cost;
+}

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java

@@ -0,0 +1,25 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Order {
+  public Item item;
+
+  /**
+   * Checks if this order has an item.
+   */
+  public boolean hasItem() {
+    if (item == null) {
+      return false;
+    } else {
+      return true;
+    }
+  }
+
+  /**
+   * Sets the item for this order.
+   */
+  public boolean setItem(Item item) {
+    boolean exists = hasItem();
+    this.item = item;
+    return exists;
+  }
+}

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class

@@ -0,0 +1,2 @@
+Source of benchmark:
+https://github.com/DiffBlue-benchmarks/java-test

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java

@@ -0,0 +1,13 @@
+CORE
+com/diffblue/javatest/nestedobjects/subpackage/Order.class
+--json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --cover location --trace
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"identifier": "__CPROVER_initialize",\n *"sourceLocation": [{][}]\n *[}],\n *"hidden": false,\n *"internal": true,\n *"stepType": "function-call",
+"internal": true,\n *"lhs": "tmp_object_factory[$][0-9]+",
+"internal": false,\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",\n *"line": "21"\n *[}],\n *"stepType": "function-call",
+"internal": false,\n *"lhs": "this",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+"internal": false,\n *"lhs": "item",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+--
+^warning: ignoring

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt

@@ -206,7 +206,11 @@ void update_internal_field(
   // set internal field to _start function-return step
   if(SSA_step.source.pc->function==goto_functionst::entry_point())
   {
-    goto_trace_step.internal=true;
+    // "__CPROVER_*" function calls in __CPROVER_start are already marked as
+    // internal. Don't mark any other function calls (i.e. "main"), function
+    // arguments or any other parts of a code_function_callt as internal.
+    if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
+      goto_trace_step.internal=true;
   }
 }