Message handler: add quote_begin, quote_end commands

jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc

@@ -3,7 +3,7 @@ Test
 --classpath ./NotHere.jar
 ^EXIT=6$
 ^SIGNAL=0$
-Warning: failed to access JAR file `./NotHere.jar'
+Warning: failed to access JAR file './NotHere.jar'
 Error: Could not find or load main class Test
 --
 --

jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc

@@ -3,7 +3,7 @@ Test
 --classpath `../../../../scripts/format_classpath.sh ./NotHere .`
 ^EXIT=0$
 ^SIGNAL=0$
-Warning: failed to access directory `./NotHere'
+Warning: failed to access directory './NotHere'
 --
 --
 Note: 'java' does not emit such a warning.

jbmc/regression/jbmc/lambda1/test_goto_functions.desc

@@ -1,14 +1,14 @@
 CORE
 Lambdatest
 --verbosity 10 --show-goto-functions --function Lambdatest.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
-lambda function reference lambda\$new\$0 in class \"Lambdatest\"
-lambda function reference lambda\$new\$1 in class \"Lambdatest\"
-lambda function reference lambda\$captureReference\$2 in class \"Lambdatest\"
-lambda function reference lambda\$captureInt\$3 in class \"Lambdatest\"
-lambda function reference lambda\$captureThisPrimitive\$4 in class \"Lambdatest\"
-lambda function reference lambda\$captureThisReference\$5 in class \"Lambdatest\"
-lambda function reference lambda\$captureAndCall\$6 in class \"Lambdatest\"
-lambda function reference lambda\$captureAndAssign\$7 in class \"Lambdatest\"
-lambda function reference lambda\$static\$0 in class \"B\"
+lambda function reference lambda\$new\$0 in class 'Lambdatest'
+lambda function reference lambda\$new\$1 in class 'Lambdatest'
+lambda function reference lambda\$captureReference\$2 in class 'Lambdatest'
+lambda function reference lambda\$captureInt\$3 in class 'Lambdatest'
+lambda function reference lambda\$captureThisPrimitive\$4 in class 'Lambdatest'
+lambda function reference lambda\$captureThisReference\$5 in class 'Lambdatest'
+lambda function reference lambda\$captureAndCall\$6 in class 'Lambdatest'
+lambda function reference lambda\$captureAndAssign\$7 in class 'Lambdatest'
+lambda function reference lambda\$static\$0 in class 'B'
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/lambda2/test.desc

@@ -1,7 +1,7 @@
 CORE symex-driven-lazy-loading-expected-failure
 org.symphonyoss.symphony.clients.model.SymStream
 --show-goto-functions --verbosity 10
-lambda function reference toSymUser in class "org\.symphonyoss\.symphony\.clients\.model\.SymStream"
+lambda function reference toSymUser in class 'org\.symphonyoss\.symphony\.clients\.model\.SymStream'
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -2101,13 +2101,11 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
 
     log.debug()
       << "lambda function reference "
-      << id2string(
-           lambda_method_handle->get_method_descriptor().base_method_name())
-      << " in class \"" << parse_tree.parsed_class.name << "\""
-      << "\n  interface type is "
-      << id2string(pool_entry(interface_type_argument.ref1).s)
-      << "\n  method type is "
-      << id2string(pool_entry(method_type_argument.ref1).s) << messaget::eom;
+      << lambda_method_handle->get_method_descriptor().base_method_name()
+      << " in class " << messaget::quote_begin << parse_tree.parsed_class.name
+      << messaget::quote_end << "\n  interface type is "
+      << pool_entry(interface_type_argument.ref1).s << "\n  method type is "
+      << pool_entry(method_type_argument.ref1).s << messaget::eom;
     parse_tree.parsed_class.add_method_handle(
       bootstrap_method_index, *lambda_method_handle);
   }

jbmc/src/java_bytecode/java_class_loader_base.cpp

@@ -34,7 +34,8 @@ void java_class_loader_baset::add_classpath_entry(
     }
     else
     {
-      log.warning() << "Warning: failed to access JAR file `" << path << "'"
+      log.warning() << "Warning: failed to access JAR file "
+                    << messaget::quote_begin << path << messaget::quote_end
                     << messaget::eom;
     }
   }
@@ -47,7 +48,8 @@ void java_class_loader_baset::add_classpath_entry(
     }
     else
     {
-      log.warning() << "Warning: failed to access directory `" << path << "'"
+      log.warning() << "Warning: failed to access directory "
+                    << messaget::quote_begin << path << messaget::quote_end
                     << messaget::eom;
     }
   }

regression/goto-cc-file-local/old-flag-name/test.desc

@@ -4,7 +4,7 @@ final-link assertion-check old-flag
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.$
+^The '--export-function-local-symbols' flag is deprecated. Please use '--export-file-local-symbols' instead.$
 --
 ^warning: ignoring
 ^\*\*\*\* WARNING: no body for function

src/ansi-c/c_typecheck_base.cpp

@@ -77,8 +77,9 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
       // versions of Visual Studio insist to use this in their C library, and
       // GCC just warns as well.
       warning().source_location = symbol.value.find_source_location();
-      warning() << "'extern' symbol '" << new_name
-                << "' should not have an initializer" << eom;
+      warning() << quote_begin << "extern" << quote_end << " symbol "
+                << quote_begin << new_name << quote_end
+                << " should not have an initializer " << eom;
     }
   }
   else if(!is_function && symbol.value.id()==ID_code)

src/ansi-c/c_typecheck_code.cpp

@@ -558,7 +558,8 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
     if(!case_is_allowed)
     {
       error().source_location = code.source_location();
-      error() << "did not expect `case' here" << eom;
+      error() << "did not expect " << quote_begin << "case" << quote_end
+              << " here" << eom;
       throw 0;
     }
 
@@ -575,7 +576,8 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(
   if(!case_is_allowed)
   {
     error().source_location = code.source_location();
-    error() << "did not expect `case' here" << eom;
+    error() << "did not expect " << quote_begin << "case" << quote_end
+            << " here" << eom;
     throw 0;
   }
 

src/ansi-c/c_typecheck_expr.cpp

@@ -812,8 +812,8 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
       if(s_it == symbol_table.symbols.end())
       {
         error().source_location = expr.source_location();
-        error() << "failed to find bound symbol `" << identifier
-                << "' in symbol table" << eom;
+        error() << "failed to find bound symbol " << quote_begin << identifier
+                << quote_end << " in symbol table" << eom;
         throw 0;
       }
 

src/cpp/cpp_instantiate_template.cpp

@@ -486,8 +486,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
     if(new_decl.member_spec().is_virtual())
     {
       error().source_location=new_decl.source_location();
-      error() << "invalid use of `virtual' in template declaration"
-              << eom;
+      error() << "invalid use of " << quote_begin << "virtual" << quote_end
+              << " in template declaration" << eom;
       throw 0;
     }
 

src/cpp/cpp_typecheck_expr.cpp

@@ -981,7 +981,8 @@ void cpp_typecheckt::typecheck_expr_this(exprt &expr)
   if(cpp_scopes.current_scope().class_identifier.empty())
   {
     error().source_location=expr.find_source_location();
-    error() << "`this' is not allowed here" << eom;
+    error() << quote_begin << "this" << quote_end << " is not allowed here"
+            << eom;
     throw 0;
   }
 

src/cpp/cpp_typecheck_function.cpp

@@ -56,8 +56,8 @@ void cpp_typecheckt::convert_parameter(
   if(symbol_table.move(symbol, new_symbol))
   {
     error().source_location=symbol.location;
-    error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\""
-            << symbol.name << "\") failed" << eom;
+    error() << "cpp_typecheckt::convert_parameter: symbol_table.move("
+            << quote_begin << symbol.name << quote_end << ") failed" << eom;
     throw 0;
   }
 

src/goto-analyzer/taint_parser.cpp

@@ -64,9 +64,13 @@ bool taint_parser(
     else
     {
       messaget message(message_handler);
-      message.error() << "taint rule must have \"kind\" which is "
-                         "\"source\" or \"sink\" or \"sanitizer\""
-                      << messaget::eom;
+      message.error() << "taint rule must have " << messaget::quote_begin
+                      << "kind" << messaget::quote_end << " which is "
+                      << messaget::quote_begin << "source"
+                      << messaget::quote_end << " or " << messaget::quote_begin
+                      << "sink" << messaget::quote_end << " or "
+                      << messaget::quote_begin << "sanitizer"
+                      << messaget::quote_end << messaget::eom;
       return true;
     }
 
@@ -75,8 +79,8 @@ bool taint_parser(
     if(function.empty())
     {
       messaget message(message_handler);
-      message.error() << "taint rule must have \"function\""
-                      << messaget::eom;
+      message.error() << "taint rule must have " << messaget::quote_begin
+                      << "function" << messaget::quote_end << messaget::eom;
       return true;
     }
     else
@@ -101,10 +105,13 @@ bool taint_parser(
     else
     {
       messaget message(message_handler);
-      message.error() << "taint rule must have \"where\""
-                      << " which is \"return_value\" or \"this\" "
-                      << "or \"parameter1\"..."
-                      << messaget::eom;
+      message.error() << "taint rule must have " << messaget::quote_begin
+                      << "where" << messaget::quote_end << " which is "
+                      << messaget::quote_begin << "return_value"
+                      << messaget::quote_end << " or " << messaget::quote_begin
+                      << "this" << messaget::quote_end << " or "
+                      << messaget::quote_begin << "parameter1"
+                      << messaget::quote_end << "..." << messaget::eom;
       return true;
     }
 

src/goto-cc/compile.cpp

@@ -662,10 +662,12 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
 
   if(cmdline.isset("export-function-local-symbols"))
   {
-    log.warning()
-      << "The `--export-function-local-symbols` flag is deprecated. "
-         "Please use `--export-file-local-symbols` instead."
-      << messaget::eom;
+    log.warning() << "The " << messaget::quote_begin
+                  << "--export-function-local-symbols" << messaget::quote_end
+                  << " flag is deprecated. "
+                     "Please use "
+                  << messaget::quote_begin << "--export-file-local-symbols"
+                  << messaget::quote_end << " instead." << messaget::eom;
   }
 }
 

src/linking/linking.cpp

@@ -679,7 +679,8 @@ void linkingt::duplicate_object_symbol(
         log.warning().source_location = new_symbol.location;
 
         log.warning() << "conflicting initializers for"
-                      << " variable '" << old_symbol.name << "'\n";
+                      << " variable " << messaget::quote_begin
+                      << old_symbol.name << messaget::quote_end << '\n';
         log.warning() << "using old value in module " << old_symbol.module
                       << " " << old_symbol.value.find_source_location() << '\n'
                       << from_expr(ns, old_symbol.name, tmp_old) << '\n';

src/linking/linking_diagnostics.cpp

@@ -370,11 +370,14 @@ void linking_diagnosticst::error(
   messaget log{message_handler};
   log.error().source_location = new_symbol.location;
 
-  log.error() << msg << " '" << old_symbol.display_name() << "'" << '\n';
-  log.error() << "old definition in module '" << old_symbol.module << "' "
+  log.error() << msg << ' ' << messaget::quote_begin
+              << old_symbol.display_name() << messaget::quote_end << '\n';
+  log.error() << "old definition in module " << messaget::quote_begin
+              << old_symbol.module << messaget::quote_end << ' '
               << old_symbol.location << '\n'
               << type_to_string_verbose(old_symbol) << '\n';
-  log.error() << "new definition in module '" << new_symbol.module << "' "
+  log.error() << "new definition in module " << messaget::quote_begin
+              << new_symbol.module << messaget::quote_end << ' '
               << new_symbol.location << '\n'
               << type_to_string_verbose(new_symbol) << messaget::eom;
 }
@@ -387,11 +390,14 @@ void linking_diagnosticst::warning(
   messaget log{message_handler};
   log.warning().source_location = new_symbol.location;
 
-  log.warning() << msg << " '" << old_symbol.display_name() << "'\n";
-  log.warning() << "old definition in module " << old_symbol.module << " "
+  log.warning() << msg << ' ' << messaget::quote_begin
+                << old_symbol.display_name() << messaget::quote_end << '\n';
+  log.warning() << "old definition in module " << messaget::quote_begin
+                << old_symbol.module << messaget::quote_end << ' '
                 << old_symbol.location << '\n'
                 << type_to_string_verbose(old_symbol) << '\n';
-  log.warning() << "new definition in module " << new_symbol.module << " "
+  log.warning() << "new definition in module " << messaget::quote_begin
+                << new_symbol.module << messaget::quote_end << ' '
                 << new_symbol.location << '\n'
                 << type_to_string_verbose(new_symbol) << messaget::eom;
 }

src/solvers/smt2/smt2_dec.cpp

@@ -215,7 +215,8 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
         const auto &message = id2string(parsed.get_sub()[1].id());
         messaget log{message_handler};
         log.error() << "SMT2 solver returned error message:\n"
-                    << "\t\"" << message << "\"" << messaget::eom;
+                    << "\t" << messaget::quote_begin << message
+                    << messaget::quote_end << messaget::eom;
         return decision_proceduret::resultt::D_ERROR;
       }
     }

src/solvers/strings/string_refinement.cpp

@@ -1107,8 +1107,9 @@ static exprt get_char_array_and_concretize(
         const auto array_expr =
           expr_try_dynamic_cast<array_exprt>(*concretized_array))
       {
-        stream << std::string(4, ' ') << "- as_string: \""
-               << string_of_array(*array_expr) << "\"\n";
+        stream << std::string(4, ' ')
+               << "- as_string: " << messaget::quote_begin
+               << string_of_array(*array_expr) << messaget::quote_end << '\n';
       }
       else
         stream << std::string(2, ' ') << "- warning: not an array"

src/statement-list/statement_list_entry_point.cpp

@@ -52,8 +52,9 @@ static bool is_main_symbol_invalid(
       if(found)
       {
         messaget message(message_handler);
-        message.error() << "main symbol `" << main_symbol_name
-                        << "' is ambiguous" << messaget::eom;
+        message.error() << "main symbol " << messaget::quote_begin
+                        << main_symbol_name << messaget::quote_end
+                        << " is ambiguous" << messaget::eom;
         return true;
       }
       else
@@ -66,7 +67,8 @@ static bool is_main_symbol_invalid(
   else
   {
     messaget message(message_handler);
-    message.error() << "main symbol `" << main_symbol_name << "' not found"
+    message.error() << "main symbol " << messaget::quote_begin
+                    << main_symbol_name << messaget::quote_end << " not found"
                     << messaget::eom;
     return true;
   }
@@ -225,8 +227,9 @@ bool statement_list_entry_point(
   if(main.value.is_nil())
   {
     messaget message(message_handler);
-    message.error() << "main symbol `" << id2string(main_symbol_name)
-                    << "' has no body" << messaget::eom;
+    message.error() << "main symbol " << messaget::quote_begin
+                    << main_symbol_name << messaget::quote_end << " has no body"
+                    << messaget::eom;
     return true;
   }
 

src/util/cout_message.cpp

@@ -70,6 +70,10 @@ console_message_handlert::console_message_handlert(bool _always_flush)
 /// \param c: ECMA-48 command code
 std::string console_message_handlert::command(unsigned c) const
 {
+  // quote_begin and quote_end
+  if(c == '<' || c == '>')
+    return "'";
+
   if(!use_SGR)
     return std::string();
 

src/util/message.cpp

@@ -95,6 +95,8 @@ const messaget::commandt messaget::bright_yellow(93);
 const messaget::commandt messaget::bright_blue(94);
 const messaget::commandt messaget::bright_magenta(95);
 const messaget::commandt messaget::bright_cyan(96);
+const messaget::commandt messaget::quote_begin('<');
+const messaget::commandt messaget::quote_end('>');
 
 /// Parse a (user-)provided string as a verbosity level and set it as the
 /// verbosity of dest.

src/util/message.h

@@ -382,6 +382,12 @@ class messaget
   /// render underlined text
   static const commandt underline;
 
+  /// start quoted text
+  static const commandt quote_begin;
+
+  /// start quoted text
+  static const commandt quote_end;
+
   mstreamt &get_mstream(unsigned message_level) const
   {
     mstream.message_level=message_level;