Test __CPROVER_ID support in the C front-end

regression/cbmc/cprover_id1/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void foo()
+{
+  static int local;
+  local = 1;
+}
+
+int main()
+{
+  // foo::1::local is the fully qualified name generated by the C front-end at
+  // this time. This is an implementation detail that could change at any time,
+  // and the test would need to be adjusted accordingly.
+  assert(__CPROVER_ID "foo::1::local" == 0);
+  foo();
+  assert(__CPROVER_ID "foo::1::local" == 1);
+}

regression/cbmc/cprover_id1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test demonstrates the use of __CPROVER_ID to form identifier names that
+would not otherwise constitute syntactically identifiers in C code.

src/ansi-c/parser.y

@@ -297,6 +297,8 @@ identifier:
           TOK_IDENTIFIER
         | TOK_CPROVER_ID TOK_STRING
         {
+          // construct an identifier from a string that would otherwise not be a
+          // valid identifier in C
           $$=$1;
           parser_stack($$).id(ID_symbol);
           irep_idt value=parser_stack($2).get(ID_value);