History variables do not check for nullness

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/history-pointer-enforce-11/main.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void foo(struct pair *p) __CPROVER_assigns(p->y)
+  __CPROVER_ensures((p != NULL) == > (p->y == __CPROVER_old(p->y) + 5))
+    __CPROVER_ensures((p == NULL) == > (p->y == __CPROVER_old(p->y)))
+{
+  if(p != NULL)
+    p->y = p->y + 5;
+}
+
+int main()
+{
+  struct pair *p = NULL;
+  foo(p);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-11/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[postcondition.\d+\] Check ensures clause\: SUCCESS$
+^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that history variables handle NULL pointers.
+History variables currently do not check for nullness while
+storing values of objects, which may lead to NULL pointer dereferences.

src/goto-instrument/contracts/contracts.cpp

@@ -394,7 +394,6 @@ void code_contractst::replace_old_parameter(
 
     const auto &parameter = to_old_expr(expr).expression();
 
-    // TODO: generalize below
     if(
       parameter.id() == ID_dereference || parameter.id() == ID_member ||
       parameter.id() == ID_symbol)