Clarify usage of history variables in error messages

Author: qinheping

regression/contracts-dfcc/reject_history_expr_in_assertions/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stddef.h>
+
+#define N 16
+
+void f(int r[N])
+{
+  for(int j = 0; j < N; j++)
+  {
+    int t = r[j];
+    __CPROVER_assert(t == __CPROVER_loop_entry(r[j]), "Initial value of r[j]");
+    r[j] = t + 1;
+  }
+}
+
+void main()
+{
+  int x[N];
+  f(x);
+}

regression/contracts-dfcc/reject_history_expr_in_assertions/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^main.c.*error: __CPROVER_loop_entry is not allowed in assume/assert.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that __CPROVER_loop_entry occurrences in assertions
+are detected and rejected.

src/ansi-c/c_typecheck_code.cpp

@@ -106,6 +106,14 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_static_assert)
   {
     PRECONDITION(code.operands().size() == 2);
+    disallow_subexpr_by_id(
+      code.op0(),
+      ID_old,
+      CPROVER_PREFIX "old is not allowed in static assert.");
+    disallow_subexpr_by_id(
+      code.op0(),
+      ID_loop_entry,
+      CPROVER_PREFIX "loop_entry is not allowed in static assert.");
 
     typecheck_expr(code.op0());
     typecheck_expr(code.op1());
@@ -142,6 +150,14 @@ void c_typecheck_baset::typecheck_code(codet &code)
     // but we allow them for the benefit of other users
     // of the typechecker.
     PRECONDITION(code.operands().size() == 1);
+    disallow_subexpr_by_id(
+      code.op0(),
+      ID_old,
+      CPROVER_PREFIX "old is not allowed in assume/assert.");
+    disallow_subexpr_by_id(
+      code.op0(),
+      ID_loop_entry,
+      CPROVER_PREFIX "loop_entry is not allowed in static assume/assert.");
     typecheck_expr(code.op0());
   }
   else