CONTRACTS: dfcc_is_cprover_symbol now uses allow lists

The result of `dfcc_is_cprover_symbol` is used to skip frame
conditon checks on symbols with special meaning. Before we
were matching symbols based on their prefix, which would
allow users to skip frame condition checks just by naming their
symbols with these prefixes. We now use a closed allow list,
and distinguish function symbolds form static var symbols.
We add test that show that variables named with __CPROVER,
__VERIFIER or nondet prefixes do not bypass frame condition
checks.

Author: Remi Delmas

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

@@ -0,0 +1,23 @@
+void foo()
+{
+  int nondet_var;
+  int __VERIFIER_var;
+  int __CPROVER_var;
+  for(int i = 10; i > 0; i--)
+    // clang-format off
+  __CPROVER_assigns(i)
+  __CPROVER_loop_invariant(0 <= i && i <= 10)
+  __CPROVER_decreases(i)
+    // clang-format on
+    {
+      nondet_var = 0;
+      __VERIFIER_var = 0;
+      __CPROVER_var = 0;
+    }
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that program variables with special name prefixes
+__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking.

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

@@ -0,0 +1,23 @@
+void foo()
+{
+  int nondet_var;
+  int __VERIFIER_var;
+  int __CPROVER_var;
+  for(int i = 10; i > 0; i--)
+    // clang-format off
+  __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)
+  __CPROVER_loop_invariant(0 <= i && i <= 10)
+  __CPROVER_decreases(i)
+    // clang-format on
+    {
+      nondet_var = 0;
+      __VERIFIER_var = 0;
+      __CPROVER_var = 0;
+    }
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that when program variables names have special prefixes
+__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them
+assignable.

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -795,7 +795,7 @@ static bool must_check_lhs_from_local_and_tracked(
       return true;
     }
     const auto &id = to_symbol_expr(expr).get_identifier();
-    if(dfcc_is_cprover_symbol(id))
+    if(dfcc_is_cprover_static_symbol(id))
     {
       // Skip the check if we have a single cprover symbol as root object
       // cprover symbols are used for generic checks instrumentation and are

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -235,7 +235,7 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const
 bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const
 {
   return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
-         (dfcc_is_cprover_symbol(id) || is_internal_symbol(id));
+         (dfcc_is_cprover_function_symbol(id) || is_internal_symbol(id));
 }
 
 void dfcc_instrumentt::instrument_harness_function(