Adds support for null pointers passed as function call parameter.

This adds support for the cases where a null pointer is passed as
a parameter to a function that may assign to it. We add checks in
goto program to handle such instances as special cases of assigns
clause handling.

Author: ArenBabikian

regression/contracts/assigns_null_pointer_01/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stddef.h>
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5))
+{
+  *x = 3;
+  if(y != NULL)
+    *y = 5;
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_null_pointer_01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for a null pointer passed as a parameter to a
+function that may assign to it. The null pointer is passed to function
+bar which has been replaced by it's function contracts, while the calling
+function foo is being checked (by enforcing it's function contracts).

regression/contracts/assigns_null_pointer_02/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stddef.h>
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5))
+{
+  *x = 3;
+  if(y != NULL)
+    *y = 5;
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+  *x = 3;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_null_pointer_02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for a null pointer passed as a parameter to a
+function that may assign to it. The null pointer is passed to function
+bar, while the calling function foo is being checked (by enforcing
+it's function contracts).

src/goto-instrument/code_contracts.cpp

@@ -1542,11 +1542,31 @@ goto_programt assigns_clauset::havoc_code(
   goto_programt havoc_statements;
   for(assigns_clause_targett *target : targets)
   {
+    //    if(target != NULL) goto x;
+    //      havoc_statements
+    // z: skip
+
+    // create the z label
+    goto_programt tmp_z;
+    goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location));
+
+    // TODO: generalize this
+    // currently only supports pointers
+    exprt condition = equal_exprt(
+      target->get_direct_pointer(),
+      null_pointer_exprt(to_pointer_type(target->get_direct_pointer().type())));
+
+    havoc_statements.add(goto_programt::make_goto(z, condition, location));
+
+    // create havoc_statements
     for(goto_programt::instructiont instruction :
         target->havoc_code(location).instructions)
     {
       havoc_statements.add(std::move(instruction));
     }
+
+    // add the z label instruction
+    havoc_statements.destructive_append(tmp_z);
   }
   return havoc_statements;
 }
@@ -1595,8 +1615,15 @@ exprt assigns_clauset::compatible_expression(
     {
       if(first_iter)
       {
-        current_target_compatible =
-          target->compatible_expression(*called_target);
+        // TODO: generalize this
+        // currently only supports pointers
+        current_target_compatible = or_exprt(
+          equal_exprt(
+            called_target->get_direct_pointer(),
+            null_pointer_exprt(
+              to_pointer_type(called_target->get_direct_pointer().type()))),
+          target->compatible_expression(*called_target));
+
         first_iter = false;
       }
       else