Check for uses of __CPROVER_ in the linter

tautschnig · tautschnig · commit d942999a576e · 2018-10-15T10:38:54.000Z
This should help avoid future code introducing literal uses of __CPROVER_ back
into the code base.
diff --git a/scripts/cpplint.py b/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)
diff --git a/src/util/cprover_prefix.h b/src/util/cprover_prefix.h
@@ -10,8 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #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
