WIP Add message warning about overriding __CPROVER things

Author: hannes-steffenhagen-diffblue

src/goto-programs/replace_function_bodies.cpp

@@ -407,12 +407,23 @@ std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
     std::vector<irep_idt> globals_to_havoc;
     namespacet ns(symbol_table);
     messaget messages(message_handler);
+    const std::regex cprover_prefix = std::regex("__CPROVER.*");
     for(auto const &symbol : symbol_table.symbols)
     {
       if(
         symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
         std::regex_match(id2string(symbol.first), globals_regex))
       {
+        if(std::regex_match(id2string(symbol.first), cprover_prefix))
+        {
+          messages.warning() << "generate function bodies: "
+                             << "matched global '"
+                             << id2string(symbol.first)
+                             << "' begins with __CPROVER, "
+                             << "havoc-ing this global may interfere"
+                             << " with analysis"
+                             << messaget::eom;
+        }
         globals_to_havoc.push_back(symbol.first);
       }
     }
@@ -465,21 +476,32 @@ void replace_function_bodies(
   goto_modelt &model,
   message_handlert &message_handler)
 {
+  messaget messages(message_handler);
+  const std::regex cprover_prefix = std::regex("__CPROVER.*");
   bool did_generate_body = false;
   for(auto &function : model.goto_functions.function_map)
   {
     if(
       !function.second.body_available() &&
       std::regex_match(id2string(function.first), functions_regex))
     {
+      if(std::regex_match(id2string(function.first), cprover_prefix))
+      {
+        messages.warning()
+          << "generate function bodies: matched function '"
+          << id2string(function.first)
+          << "' begins with __CPROVER "
+          << "the generated body for this function "
+          << "may interfere with analysis"
+          << messaget::eom;
+      }
       did_generate_body = true;
       generate_function_body.generate_function_body(
         function.second, model.symbol_table, function.first);
     }
   }
   if(!did_generate_body)
   {
-    messaget messages(message_handler);
     messages.warning()
       << "generate function bodies: No function name matched regex"
       << messaget::eom;