Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -21,7 +21,7 @@ void java_internal_additions(symbol_table_baset &dest)
 
   {
     symbolt symbol;
-    symbol.base_name="__CPROVER_rounding_mode";
+    symbol.base_name = CPROVER_PREFIX "rounding_mode";
     symbol.name=CPROVER_PREFIX "rounding_mode";
     symbol.type=signed_int_type();
     symbol.mode=ID_C;
@@ -35,7 +35,7 @@ void java_internal_additions(symbol_table_baset &dest)
 
   {
     symbolt symbol;
-    symbol.base_name="__CPROVER_malloc_object";
+    symbol.base_name = CPROVER_PREFIX "malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
     symbol.type=pointer_type(empty_typet());
     symbol.mode=ID_C;

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -77,11 +77,13 @@ SCENARIO(
               std::regex_replace(line, spaces, " "), numbers, ""));
         }
 
-        const std::vector<std::string> reference_code = { // NOLINT
+        // clang-format off
+        // NOLINTNEXTLINE
+        const std::vector<std::string> reference_code = {
           "int tmp_object_factory;",
           "tmp_object_factory = NONDET(int);",
-          "__CPROVER_assume(tmp_object_factory >= 0);",
-          "__CPROVER_assume(tmp_object_factory <= 20);",
+          CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
+          CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
           "char (*string_data_pointer)[INFINITY()];",
           "string_data_pointer = "
             "ALLOCATE(char [INFINITY()], INFINITY(), false);",
@@ -98,6 +100,7 @@ SCENARIO(
             "=\"java::java.lang.String\" },"
             " .length=tmp_object_factory, "
             ".data=*string_data_pointer };"};
+        // clang-format on
 
         for(std::size_t i = 0;
             i < code_string.size() && i < reference_code.size();

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/analyses/custom_bitvector_analysis.cpp

@@ -320,10 +320,11 @@ void custom_bitvector_domaint::transform(
       {
         const irep_idt &identifier=to_symbol_expr(function).get_identifier();
 
-        if(identifier=="__CPROVER_set_must" ||
-           identifier=="__CPROVER_clear_must" ||
-           identifier=="__CPROVER_set_may" ||
-           identifier=="__CPROVER_clear_may")
+        if(
+          identifier == CPROVER_PREFIX "set_must" ||
+          identifier == CPROVER_PREFIX "clear_must" ||
+          identifier == CPROVER_PREFIX "set_may" ||
+          identifier == CPROVER_PREFIX "clear_may")
         {
           if(code_function_call.arguments().size()==2)
           {
@@ -333,13 +334,13 @@ void custom_bitvector_domaint::transform(
             // initialize to make Visual Studio happy
             modet mode = modet::SET_MUST;
 
-            if(identifier=="__CPROVER_set_must")
+            if(identifier == CPROVER_PREFIX "set_must")
               mode=modet::SET_MUST;
-            else if(identifier=="__CPROVER_clear_must")
+            else if(identifier == CPROVER_PREFIX "clear_must")
               mode=modet::CLEAR_MUST;
-            else if(identifier=="__CPROVER_set_may")
+            else if(identifier == CPROVER_PREFIX "set_may")
               mode=modet::SET_MAY;
-            else if(identifier=="__CPROVER_clear_may")
+            else if(identifier == CPROVER_PREFIX "clear_may")
               mode=modet::CLEAR_MAY;
             else
               UNREACHABLE;

src/analyses/escape_analysis.cpp

@@ -11,16 +11,20 @@ Author: Daniel Kroening, [email protected]
 
 #include "escape_analysis.h"
 
+#include <util/cprover_prefix.h>
 #include <util/simplify_expr.h>
 
 bool escape_domaint::is_tracked(const symbol_exprt &symbol)
 {
   const irep_idt &identifier=symbol.get_identifier();
-  if(identifier=="__CPROVER_memory_leak" ||
-     identifier=="__CPROVER_malloc_object" ||
-     identifier=="__CPROVER_dead_object" ||
-     identifier=="__CPROVER_deallocated")
+  if(
+    identifier == CPROVER_PREFIX "memory_leak" ||
+    identifier == CPROVER_PREFIX "malloc_object" ||
+    identifier == CPROVER_PREFIX "dead_object" ||
+    identifier == CPROVER_PREFIX "deallocated")
+  {
     return false;
+  }
 
   return true;
 }
@@ -217,7 +221,7 @@ void escape_domaint::transform(
       if(function.id()==ID_symbol)
       {
         const irep_idt &identifier=to_symbol_expr(function).get_identifier();
-        if(identifier=="__CPROVER_cleanup")
+        if(identifier == CPROVER_PREFIX "cleanup")
         {
           if(code_function_call.arguments().size()==2)
           {

src/ansi-c/ansi_c_internal_additions.cpp

@@ -109,77 +109,78 @@ const char windows_builtin_headers[]=
 
 static std::string architecture_string(const std::string &value, const char *s)
 {
-  return std::string("const char *__CPROVER_architecture_")+
-         std::string(s)+
-         "=\""+value+"\";\n";
+  return std::string("const char *" CPROVER_PREFIX "architecture_") +
+         std::string(s) + "=\"" + value + "\";\n";
 }
 
 template <typename T>
 static std::string architecture_string(T value, const char *s)
 {
-  return std::string("const int __CPROVER_architecture_")+
-         std::string(s)+
-         "="+std::to_string(value)+";\n";
+  return std::string("const int " CPROVER_PREFIX "architecture_") +
+         std::string(s) + "=" + std::to_string(value) + ";\n";
 }
 
 void ansi_c_internal_additions(std::string &code)
 {
+  // clang-format off
   // do the built-in types and variables
   code+=
     "# 1 \"<built-in-additions>\"\n"
-    "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
+    "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
     "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
-      " __CPROVER_ssize_t;\n"
-    "const unsigned __CPROVER_constant_infinity_uint;\n"
-    "typedef void __CPROVER_integer;\n"
-    "typedef void __CPROVER_rational;\n"
-    "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
-    "unsigned long __CPROVER_next_thread_id=0;\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
+      " " CPROVER_PREFIX "ssize_t;\n"
+    "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
+    "typedef void " CPROVER_PREFIX "integer;\n"
+    "typedef void " CPROVER_PREFIX "rational;\n"
+    CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
+    "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
+    "extern unsigned char " CPROVER_PREFIX "memory["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // malloc
-    "const void *__CPROVER_deallocated=0;\n"
-    "const void *__CPROVER_dead_object=0;\n"
-    "const void *__CPROVER_malloc_object=0;\n"
-    "__CPROVER_size_t __CPROVER_malloc_size;\n"
-    "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
-    "const void *__CPROVER_memory_leak=0;\n"
-    "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
+    "const void *" CPROVER_PREFIX "deallocated=0;\n"
+    "const void *" CPROVER_PREFIX "dead_object=0;\n"
+    "const void *" CPROVER_PREFIX "malloc_object=0;\n"
+    CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
+    "const void *" CPROVER_PREFIX "memory_leak=0;\n"
+    "void *" CPROVER_PREFIX "allocate("
+      CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
 
     // this is ANSI-C
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
+    "extern " CPROVER_PREFIX "thread_local const char __func__["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // this is GCC
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
+    "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
+    "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // float stuff
-    "int __CPROVER_thread_local __CPROVER_rounding_mode="+
+    "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
       std::to_string(config.ansi_c.rounding_mode)+";\n"
 
     // pipes, write, read, close
-    "struct __CPROVER_pipet {\n"
+    "struct " CPROVER_PREFIX "pipet {\n"
     "  _Bool widowed;\n"
     "  char data[4];\n"
     "  short next_avail;\n"
     "  short next_unread;\n"
     "};\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
+    "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
     // offset to make sure we don't collide with other fds
-    "extern const int __CPROVER_pipe_offset;\n"
-    "unsigned __CPROVER_pipe_count=0;\n"
+    "extern const int " CPROVER_PREFIX "pipe_offset;\n"
+    "unsigned " CPROVER_PREFIX "pipe_count=0;\n"
     "\n"
     // This function needs to be declared, or otherwise can't be called
     // by the entry-point construction.
     "void " INITIALIZE_FUNCTION "(void);\n"
     "\n";
+  // clang-format on
 
   // GCC junk stuff, also for CLANG and ARM
   if(
@@ -201,13 +202,13 @@ void ansi_c_internal_additions(std::string &code)
       // For clang, __float128 is a keyword.
       // For gcc, this is a typedef and not a keyword.
       if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
-        code += "typedef __CPROVER_Float128 __float128;\n";
+        code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
     }
     else if(config.ansi_c.arch == "ppc64le")
     {
       // https://patchwork.ozlabs.org/patch/792295/
       if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
-        code += "typedef __CPROVER_Float128 __ieee128;\n";
+        code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
     }
     else if(config.ansi_c.arch == "hppa")
     {
@@ -225,7 +226,7 @@ void ansi_c_internal_additions(std::string &code)
       // clang doesn't do __float80
       // Note that __float80 is a typedef, and not a keyword.
       if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
-        code += "typedef __CPROVER_Float64x __float80;\n";
+        code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
     }
 
     // On 64-bit systems, gcc has typedefs

src/ansi-c/c_typecheck_base.cpp

@@ -771,7 +771,7 @@ void c_typecheck_baset::typecheck_declaration(
         ret_type=to_code_type(new_symbol.type).return_type();
       assert(parameter_map.empty());
       if(ret_type.id()!=ID_empty)
-        parameter_map["__CPROVER_return_value"]=ret_type;
+        parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
       typecheck_spec_expr(contract, ID_C_spec_ensures);
       parameter_map.clear();
 

src/ansi-c/c_typecheck_type.cpp

@@ -1508,11 +1508,11 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
     type.set(ID_C_alignment, alignment);
 
   // CPROVER extensions
-  if(symbol.base_name=="__CPROVER_rational")
+  if(symbol.base_name == CPROVER_PREFIX "rational")
   {
     type=rational_typet();
   }
-  else if(symbol.base_name=="__CPROVER_integer")
+  else if(symbol.base_name == CPROVER_PREFIX "integer")
   {
     type=integer_typet();
   }

src/ansi-c/cprover_library.cpp

@@ -25,7 +25,7 @@ static std::string get_cprover_library_text(
     "#undef inline\n";
 
   if(config.ansi_c.string_abstraction)
-    library_text << "#define __CPROVER_STRING_ABSTRACTION\n";
+    library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
 
   // cprover_library.inc may not have been generated when running Doxygen, thus
   // make Doxygen skip this part