Check for uses of __CPROVER_ in the linter

This should help avoid future code introducing literal uses of __CPROVER_ back
into the code base.

Author: tautschnig

scripts/cpplint.py

@@ -4653,6 +4653,23 @@ def CheckAssert(filename, clean_lines, linenum, error):
 
 
 
+def Check__CPROVER_(filename, clean_lines, linenum, error):
+  """Check for uses of __CPROVER_.
+
+  Args:
+    filename: The name of the current file.
+    clean_lines: A CleansedLines instance containing the file.
+    linenum: The number of the line to check.
+    error: The function to call with any errors found.
+  """
+  line = clean_lines.lines[linenum]
+  match = Match(r'.*__CPROVER_.*', line)
+  if match:
+    error(filename, linenum, 'build/deprecated', 4,
+          'use CPROVER_PREFIX instead of __CPROVER_')
+
+
+
 def GetLineWidth(line):
   """Determines the width of the line in column positions.
 
@@ -4880,6 +4897,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state,
   #CheckCheck(filename, clean_lines, linenum, error)
   CheckAltTokens(filename, clean_lines, linenum, error)
   CheckAssert(filename, clean_lines, linenum, error)
+  Check__CPROVER_(filename, clean_lines, linenum, error)
   classinfo = nesting_state.InnermostClass()
   if classinfo:
     CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error)

src/util/cprover_prefix.h

@@ -10,8 +10,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_CPROVER_PREFIX_H
 #define CPROVER_UTIL_CPROVER_PREFIX_H
 
+// NOLINTNEXTLINE(build/deprecated)
 #define CPROVER_PREFIX "__CPROVER_"
+// NOLINTNEXTLINE(build/deprecated)
 #define CPROVER_FKT_PREFIX "__CPROVER_fkt_"
+// NOLINTNEXTLINE(build/deprecated)
 #define CPROVER_MACRO_PREFIX "__CPROVER_macro_"
 
 #endif // CPROVER_UTIL_CPROVER_PREFIX_H