diff --git a/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc index 683e08b45cf..4a862844e86 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc +++ b/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 -- -- diff --git a/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc index 1d633f73cdf..7b3ac7b6024 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc +++ b/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. diff --git a/jbmc/regression/jbmc/lambda1/test_goto_functions.desc b/jbmc/regression/jbmc/lambda1/test_goto_functions.desc index 99832c590ae..c7be86960cd 100644 --- a/jbmc/regression/jbmc/lambda1/test_goto_functions.desc +++ b/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$ diff --git a/jbmc/regression/jbmc/lambda2/test.desc b/jbmc/regression/jbmc/lambda2/test.desc index fe65b028d03..91af0622382 100644 --- a/jbmc/regression/jbmc/lambda2/test.desc +++ b/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$ -- diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 2fe7ccafbf7..f91c953e70d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/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); } diff --git a/jbmc/src/java_bytecode/java_class_loader_base.cpp b/jbmc/src/java_bytecode/java_class_loader_base.cpp index 57a8a31d37b..24efaaf881c 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.cpp +++ b/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; } } diff --git a/regression/goto-cc-file-local/old-flag-name/test.desc b/regression/goto-cc-file-local/old-flag-name/test.desc index fa6f0e20b17..4fa9efb29f7 100644 --- a/regression/goto-cc-file-local/old-flag-name/test.desc +++ b/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 diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index f11e08f7e14..b446e6dddcd 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/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) diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index c969bf12575..d85ad8d2c7d 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/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; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1534260a50e..e8f5b2074e9 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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; } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 4328428b326..b8239e1917f 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/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; } diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 2685771889c..5549c28b431 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/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; } diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index e7968615198..154b037dae4 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/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; } diff --git a/src/goto-analyzer/taint_parser.cpp b/src/goto-analyzer/taint_parser.cpp index 168975d5dcb..eef64800cc1 100644 --- a/src/goto-analyzer/taint_parser.cpp +++ b/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; } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3631189d812..0a49ec521ab 100644 --- a/src/goto-cc/compile.cpp +++ b/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; } } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 65fc1a8f4d4..1491c6bdb5c 100644 --- a/src/linking/linking.cpp +++ b/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'; diff --git a/src/linking/linking_diagnostics.cpp b/src/linking/linking_diagnostics.cpp index 626c2e3324c..0ba3a68577f 100644 --- a/src/linking/linking_diagnostics.cpp +++ b/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; } diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index e467db8e5ba..aefb5a237e9 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/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; } } diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index e1980bed5f4..48b20805268 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/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(*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" diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 7bb7b1b1cef..97a2323297a 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/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; } diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 641c5c35c93..c098e285d60 100644 --- a/src/util/cout_message.cpp +++ b/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(); diff --git a/src/util/message.cpp b/src/util/message.cpp index 38ab1cfd26d..d87958ac522 100644 --- a/src/util/message.cpp +++ b/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. diff --git a/src/util/message.h b/src/util/message.h index ec1624855e8..8051e0a5e94 100644 --- a/src/util/message.h +++ b/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; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 8d92e33b816..5478ba4c404 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -96,10 +96,75 @@ class ui_message_handlert : public message_handlert std::string command(unsigned c) const override { - if(message_handler) - return message_handler->command(c); - else + if(!message_handler) return std::string(); + + switch(_ui) + { + case uit::PLAIN: + switch(c) + { + case '<': // fall through + case '>': + return "'"; + } + break; + case uit::XML_UI: + switch(c) + { + case 0: // reset + case 1: // bold + case 2: // faint + case 3: // italic + case 4: // underline + case 31: // red + case 32: // green + case 33: // yellow + case 34: // blue + case 35: // magenta + case 36: // cyan + case 91: // bright_red + case 92: // bright_green + case 93: // bright_yellow + case 94: // bright_blue + case 95: // bright_magenta + case 96: // bright_cyan + return std::string(); + case '<': // quote_begin + return "'"; // could use something like here + case '>': // quote_end + return "'"; // could use something like here + } + break; + case uit::JSON_UI: + switch(c) + { + case 0: // reset + case 1: // bold + case 2: // faint + case 3: // italic + case 4: // underline + case 31: // red + case 32: // green + case 33: // yellow + case 34: // blue + case 35: // magenta + case 36: // cyan + case 91: // bright_red + case 92: // bright_green + case 93: // bright_yellow + case 94: // bright_blue + case 95: // bright_magenta + case 96: // bright_cyan + return std::string(); + case '<': // quote_begin + case '>': // quote_end + return "'"; + } + break; + } + + return message_handler->command(c); } };