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.