Function contracts: allow history variables for typecast and constant expressions.

Author: Remi Delmas

regression/contracts/history-constant/main.c

@@ -0,0 +1,15 @@
+#include <stdio.h>
+
+int foo(int l) __CPROVER_requires(-10 <= l && l <= 10) __CPROVER_ensures(
+  __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(10))
+{
+  return l + 10;
+}
+
+int main()
+{
+  int l;
+  __CPROVER_assume(-10 <= l && l <= 10);
+  foo(l);
+  return 0;
+}

regression/contracts/history-constant/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of constant expressions is not supported yet
+--
+This test checks that history variables are supported for constant expressions.

regression/contracts/history-typecast/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+long bar(long l, long r) __CPROVER_requires(-10 <= l && l <= 10)
+  __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return l + r;
+}
+
+int foo(int l, int r) __CPROVER_requires(-10 <= l && l <= 10)
+  __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return bar((long)l, (long)r);
+}
+
+int main()
+{
+  int n;
+  __CPROVER_assume(-10 <= n && n <= 10);
+  foo(n, n);
+  return 0;
+}

regression/contracts/history-typecast/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-call-with-contract bar --enforce-contract foo 
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of typecast expressions is not supported yet
+--
+This test checks that history variables are supported for typecast expressions.

src/goto-instrument/contracts/contracts.cpp

@@ -562,9 +562,10 @@ void code_contractst::replace_history_parameter(
   {
     const auto &parameter = to_history_expr(expr, id).expression();
 
+    const auto &id = parameter.id();
     if(
-      parameter.id() == ID_dereference || parameter.id() == ID_member ||
-      parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
+      id == ID_dereference || id == ID_member || id == ID_symbol ||
+      id == ID_ptrmember || id == ID_constant || id == ID_typecast)
     {
       auto it = parameter2history.find(parameter);