Adds support for pointer history variables in function contracts

This adds support for history variables in function contracts.
History variables are (1) declared and (2) assigned to the
value that their corresponding variable has at function call time.
Currently, only pointers are supported.

Author: ArenBabikian

regression/contracts/history-pointer-both-01/main.c

@@ -0,0 +1,20 @@
+#include <stdio.h>
+
+void bar(int *l) __CPROVER_assigns(*l) __CPROVER_requires(l != NULL)
+  __CPROVER_ensures(__CPROVER_old(*l) == *l)
+{
+}
+
+void foo(int *n) __CPROVER_assigns(*n) __CPROVER_requires(n != NULL)
+  __CPROVER_ensures(__CPROVER_old(*n) == *n)
+{
+  bar(n);
+}
+
+int main()
+{
+  int m;
+  foo(&m);
+
+  return 0;
+}

regression/contracts/history-pointer-both-01/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSUME tmp_cc\$\d != \(\(signed int \*\)NULL\)
+ASSERT n != \(\(signed int \*\)NULL\)
+ASSUME tmp_cc == \*n
+ASSERT tmp_cc\$\d == \*tmp_cc\$\d
+--
+--
+Verification:
+This test checks that history variables are supported for parameters of the
+the function under test. By using the --enforce-all-contracts flag,
+the post-condition (which contains the history variable) is asserted.
+In this case, this assertion should pass.

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

@@ -0,0 +1,13 @@
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x == __CPROVER_old(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT \*tmp_cc\$\d == tmp_cc\$\d \+ 5
+--
+--
+Verification:
+This test checks that history variables are supported for parameters of the
+the function under test. By using the --enforce-all-contracts flag,
+the post-condition (which contains the history variable) is asserted.
+In this case, this assertion should pass.

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

@@ -0,0 +1,13 @@
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x < __CPROVER_old(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+ASSERT \*tmp_cc\$\d < tmp_cc\$\d \+ 5
+--
+--
+Verification:
+This test checks that history variables are supported for parameters of the
+the function under test. By using the --enforce-all-contracts flag,
+the post-condition (which contains the history variable) is asserted.
+In this case, this assertion should fail.

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

@@ -0,0 +1,16 @@
+#include <limits.h>
+
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_requires(*x > 0 && *x < INT_MAX - 5) __CPROVER_ensures(
+    *x >= __CPROVER_old(*x) + 4 && *x <= __CPROVER_old(*x) + 6)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT tmp_if_expr\$\d
+--
+--
+Verification:
+This test checks that history variables are supported in the case where a
+history variable is referred to multiple times within an ensures clause.
+By using the --enforce-all-contracts flag, the post-condition (which contains
+the history variable) is asserted. In this case, this assertion should pass.

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

@@ -0,0 +1,15 @@
+void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
+  __CPROVER_ensures(*x == __CPROVER_old(*y) + 1 && *y == __CPROVER_old(*x) + 2)
+{
+  int x_initial = *x;
+  *x = *y + 1;
+  *y = x_initial + 2;
+}
+
+int main()
+{
+  int x, y;
+  foo(&x, &y);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT tmp_if_expr
+--
+--
+Verification:
+This test checks that history variables are supported in the case where the
+function under test has multiple parameters. By using the
+--enforce-all-contracts flag, the post-condition (which contains the history
+variables) is asserted. In this case, this assertion should pass.