From c4cd7aeca6ec7a60911c95891be4ef78c62d74f2 Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 4 Jul 2019 17:57:15 +0100 Subject: [PATCH 1/3] Do not use backtick as opening single quote Replace it with '. For example, This changes an error message from failed to load class `java.nio.file.Path' to failed to load class 'java.nio.file.Path' The reason is that the convention of using ` for opening single quotes looks odd in most modern fonts. For more discussion please read: https://www.cl.cam.ac.uk/~mgk25/ucs/quotes.html --- .../test-array-value-annotation-on-class.desc | 4 +- .../test-array-value-annotation-on-field.desc | 4 +- ...test-array-value-annotation-on-method.desc | 4 +- ...t-array-value-annotation-on-parameter.desc | 4 +- .../test-class-value-annotation-on-class.desc | 2 +- .../test-class-value-annotation-on-field.desc | 2 +- ...test-class-value-annotation-on-method.desc | 2 +- ...t-class-value-annotation-on-parameter.desc | 2 +- .../test.desc | 2 +- .../jbmc/classpath-invalid/test-jar.desc | 2 +- .../jbmc/classpath-invalid/test-path.desc | 2 +- .../jbmc/classpath-jar-entry-method/test.desc | 6 +- .../test_class.desc | 2 +- .../test_jar_main_class.desc | 2 +- .../jbmc/generics_type_param/test.desc | 6 +- .../jbmc/overlay-class/correct-test.desc | 4 +- .../jbmc/overlay-class/duplicate-test.desc | 4 +- .../jbmc/overlay-class/misordered-test.desc | 4 +- .../jbmc/overlay-class/unmarked-test.desc | 4 +- .../src/janalyzer/janalyzer_parse_options.cpp | 8 +- .../java_bytecode/java_bytecode_parser.cpp | 4 +- jbmc/src/java_bytecode/java_class_loader.cpp | 11 +- .../java_bytecode/java_class_loader_base.cpp | 6 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 +- regression/ansi-c/Array_Declarator8/test.desc | 2 +- .../ansi-c/linking_conflicts1/test.desc | 4 +- .../ansi-c/linking_conflicts2/test.desc | 2 +- regression/ansi-c/message_handling1/test.desc | 2 +- regression/ansi-c/static2/test.desc | 2 +- regression/ansi-c/static3/test.desc | 2 +- regression/cbmc-cover/mcdc1/test.desc | 12 +- regression/cbmc-cover/mcdc10/test.desc | 8 +- regression/cbmc-cover/mcdc11/test.desc | 12 +- regression/cbmc-cover/mcdc12/test.desc | 18 +- regression/cbmc-cover/mcdc13/test.desc | 8 +- regression/cbmc-cover/mcdc14/test.desc | 4 +- regression/cbmc-cover/mcdc2/test.desc | 8 +- regression/cbmc-cover/mcdc3/test.desc | 6 +- regression/cbmc-cover/mcdc4/test.desc | 10 +- regression/cbmc-cover/mcdc5/test.desc | 10 +- regression/cbmc-cover/mcdc6/test.desc | 4 +- regression/cbmc-cover/mcdc7/test.desc | 8 +- regression/cbmc-cover/mcdc8/test.desc | 8 +- regression/cbmc-cover/mcdc9/test.desc | 10 +- .../cbmc/array-function-parameters/test.desc | 2 +- regression/cbmc/pragma_cprover1/test.desc | 2 +- .../name-clash-with-suffix/test.desc | 2 +- .../goto-cc-file-local/name-clash/test.desc | 4 +- .../goto-instrument/inline_05/test.desc | 4 +- .../goto-instrument/inline_06/test.desc | 4 +- .../goto-instrument/inline_07/test.desc | 4 +- .../goto-instrument/inline_09/test.desc | 2 +- .../function-application2.desc | 2 +- src/analyses/goto_check.cpp | 4 +- src/analyses/goto_rw.cpp | 4 +- src/ansi-c/ansi_c_entry_point.cpp | 6 +- src/ansi-c/builtin_factory.cpp | 4 +- src/ansi-c/c_preprocess.cpp | 2 +- src/ansi-c/c_typecheck_base.cpp | 31 ++-- src/ansi-c/c_typecheck_code.cpp | 2 +- src/ansi-c/c_typecheck_expr.cpp | 157 ++++++++---------- src/ansi-c/c_typecheck_initializer.cpp | 46 +++-- src/ansi-c/c_typecheck_type.cpp | 20 +-- src/ansi-c/c_typecheck_typecast.cpp | 6 +- .../literals/convert_string_literal.cpp | 4 +- src/cbmc/cbmc_parse_options.cpp | 4 +- src/cpp/cpp_constructor.cpp | 4 +- src/cpp/cpp_declarator_converter.cpp | 42 ++--- src/cpp/cpp_destructor.cpp | 4 +- src/cpp/cpp_instantiate_template.cpp | 15 +- src/cpp/cpp_scopes.h | 2 +- src/cpp/cpp_typecheck_bases.cpp | 2 +- src/cpp/cpp_typecheck_code.cpp | 8 +- src/cpp/cpp_typecheck_compound_type.cpp | 20 +-- src/cpp/cpp_typecheck_constructor.cpp | 6 +- src/cpp/cpp_typecheck_conversions.cpp | 9 +- src/cpp/cpp_typecheck_declaration.cpp | 5 +- src/cpp/cpp_typecheck_enum_type.cpp | 9 +- src/cpp/cpp_typecheck_expr.cpp | 68 ++++---- src/cpp/cpp_typecheck_initializer.cpp | 16 +- src/cpp/cpp_typecheck_namespace.cpp | 14 +- src/cpp/cpp_typecheck_resolve.cpp | 63 +++---- src/cpp/cpp_typecheck_template.cpp | 36 ++-- src/cpp/cpp_typecheck_using.cpp | 6 +- src/cpp/parse.cpp | 2 +- .../goto_analyzer_parse_options.cpp | 8 +- src/goto-analyzer/show_on_source.cpp | 2 +- src/goto-analyzer/taint_analysis.cpp | 6 +- src/goto-cc/compile.cpp | 23 ++- src/goto-cc/ms_cl_cmdline.cpp | 9 +- src/goto-cc/ms_link_cmdline.cpp | 6 +- .../function_call_harness_generator.cpp | 2 +- src/goto-harness/goto_harness_generator.cpp | 2 +- .../goto_harness_parse_options.cpp | 4 +- .../memory_snapshot_harness_generator.cpp | 2 +- src/goto-harness/recursive_initialization.cpp | 4 +- .../cover_instrument_condition.cpp | 4 +- .../cover_instrument_decision.cpp | 4 +- src/goto-instrument/cover_instrument_mcdc.cpp | 6 +- .../cover_instrument_other.cpp | 2 +- src/goto-instrument/function.cpp | 2 +- .../goto_instrument_parse_options.cpp | 10 +- src/goto-instrument/interrupt.cpp | 9 +- src/goto-instrument/undefined_functions.cpp | 2 +- src/goto-programs/builtin_functions.cpp | 69 ++++---- src/goto-programs/format_strings.cpp | 4 +- src/goto-programs/goto_convert.cpp | 4 +- src/goto-programs/goto_inline_class.cpp | 8 +- src/goto-programs/initialize_goto_model.cpp | 8 +- src/goto-programs/interpreter.cpp | 2 +- src/goto-programs/lazy_goto_model.cpp | 4 +- src/goto-programs/read_bin_goto_object.cpp | 6 +- src/goto-programs/read_goto_binary.cpp | 5 +- src/goto-programs/write_goto_binary.cpp | 3 +- src/goto-symex/symex_assign.cpp | 4 +- src/goto-symex/symex_function_call.cpp | 2 +- src/jsil/jsil_entry_point.cpp | 10 +- src/jsil/jsil_typecheck.cpp | 62 +++---- src/langapi/mode.cpp | 2 +- src/linking/linking.cpp | 16 +- .../memory_analyzer_parse_options.cpp | 2 +- src/pointer-analysis/value_set.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fivr.cpp | 2 +- src/pointer-analysis/value_set_fivrns.cpp | 2 +- src/solvers/flattening/arrays.cpp | 11 +- src/solvers/flattening/boolbv_with.cpp | 2 +- src/solvers/prop/prop_conv_solver.cpp | 2 +- src/solvers/refinement/refine_arithmetic.cpp | 4 +- src/solvers/smt2/smt2_conv.cpp | 2 +- src/solvers/smt2/smt2_parser.cpp | 44 ++--- src/solvers/smt2/smt2_solver.cpp | 4 +- src/solvers/smt2/smt2_tokenizer.cpp | 2 +- src/symtab2gb/symtab2gb_parse_options.cpp | 8 +- src/util/array_name.cpp | 4 +- src/util/config.cpp | 6 +- src/util/get_module.cpp | 6 +- src/util/parser.cpp | 8 +- src/util/string_utils.cpp | 2 +- 139 files changed, 603 insertions(+), 710 deletions(-) diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc index 3c08765123f..75bb04e762d 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc @@ -3,8 +3,8 @@ ArrayValueAnnotationOnClass.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class -Getting class `MyClassB' from file \.[\\/]MyClassB\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassB' from file \.[\\/]MyClassB\.class -- -- This test checks that element classes of arrays that are given as values of a class-level annotation diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc index 0774f63bd18..64ea78318c7 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc @@ -3,8 +3,8 @@ ArrayValueAnnotationOnField.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class -Getting class `MyClassB' from file \.[\\/]MyClassB\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassB' from file \.[\\/]MyClassB\.class -- -- This test checks that element classes of arrays that are given as values of a field-level annotation diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc index 9c75a2df3ae..08d5ddf654f 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc @@ -3,8 +3,8 @@ ArrayValueAnnotationOnMethod.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class -Getting class `MyClassB' from file \.[\\/]MyClassB\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassB' from file \.[\\/]MyClassB\.class -- -- This test checks that element classes of arrays that are given as values of a method-level diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc index 20defa487e0..c0e7f2e3041 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc @@ -3,8 +3,8 @@ ArrayValueAnnotationOnParameter.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class -Getting class `MyClassB' from file \.[\\/]MyClassB\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassB' from file \.[\\/]MyClassB\.class -- -- This test checks that element classes of arrays that are given as values of an annotation at method diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc index 5139fd0a95c..d3a3cb79986 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc @@ -3,7 +3,7 @@ ClassValueAnnotationOnClass.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class -- MyClassB -- diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc index b825f7af174..3bb7589b6d1 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc @@ -3,7 +3,7 @@ ClassValueAnnotationOnField.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class -- MyClassB -- diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc index 4c1565f6e9c..7b2db4f454d 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc @@ -3,7 +3,7 @@ ClassValueAnnotationOnMethod.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class -- MyClassB -- diff --git a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc index c1897af8584..d7a3b9e4dca 100644 --- a/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc +++ b/jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc @@ -3,7 +3,7 @@ ClassValueAnnotationOnParameter.class --verbosity 10 ^EXIT=6$ ^SIGNAL=0$ -Getting class `MyClassA' from file \.[\\/]MyClassA\.class +Getting class 'MyClassA' from file \.[\\/]MyClassA\.class -- MyClassB -- diff --git a/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc b/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc index 8ecc46cd9dd..63419788983 100644 --- a/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc +++ b/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc @@ -5,7 +5,7 @@ Test.class ^SIGNAL=0$ -- Java main class: Test -failed to open input file `Test.class' +failed to open input file 'Test.class' -- Test.class is not in the right directory corresponding to its package. Issue: 2864 diff --git a/jbmc/regression/jbmc/classpath-invalid/test-jar.desc b/jbmc/regression/jbmc/classpath-invalid/test-jar.desc index ad020054856..f0545562fa7 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test-jar.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test-jar.desc @@ -4,7 +4,7 @@ Test.class ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ -^failed to load class `Test'$ +^failed to load class 'Test'$ -- -- symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/jbmc/regression/jbmc/classpath-invalid/test-path.desc b/jbmc/regression/jbmc/classpath-invalid/test-path.desc index 282ae0209f8..f3b70faa9d3 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test-path.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test-path.desc @@ -4,7 +4,7 @@ Test.class ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ -^failed to load class `Test'$ +^failed to load class 'Test'$ -- -- symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/jbmc/regression/jbmc/classpath-jar-entry-method/test.desc b/jbmc/regression/jbmc/classpath-jar-entry-method/test.desc index 71e0940787b..688edab51ba 100644 --- a/jbmc/regression/jbmc/classpath-jar-entry-method/test.desc +++ b/jbmc/regression/jbmc/classpath-jar-entry-method/test.desc @@ -4,10 +4,10 @@ jar_file.jar ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -Getting class `RelevantClass' from JAR jar_file.jar -Getting class `RelatedClass' from JAR jar_file.jar +Getting class 'RelevantClass' from JAR jar_file.jar +Getting class 'RelatedClass' from JAR jar_file.jar -- -Getting class `IrrelevantClass' from JAR jar_file.jar +Getting class 'IrrelevantClass' from JAR jar_file.jar -- This test checks that when JBMC is given a jar file as an argument and an entry method is specified with --function, only classes that are (possibly diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc index 56820974f10..ff0da58f7f6 100644 --- a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc +++ b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc @@ -5,7 +5,7 @@ Test.class ^SIGNAL=0$ -- Java main class: Test -failed to open input file `Test.class' +failed to open input file 'Test.class' -- Test.class is not in the right directory corresponding to its package. Issue: 2864 diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc index e7befbb7412..71d464cde24 100644 --- a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc +++ b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc @@ -5,7 +5,7 @@ test.jar ^SIGNAL=0$ -- Java main class: Test -failed to open input file `Test.class' +failed to open input file 'Test.class' -- Test.class is not in the right directory corresponding to its package. Issue: 2864 diff --git a/jbmc/regression/jbmc/generics_type_param/test.desc b/jbmc/regression/jbmc/generics_type_param/test.desc index ef3971e4559..9e1b87c986a 100644 --- a/jbmc/regression/jbmc/generics_type_param/test.desc +++ b/jbmc/regression/jbmc/generics_type_param/test.desc @@ -7,6 +7,6 @@ Reading class AWrapper Reading class FWrapper Reading class IWrapper -- -failed to load class \`AWrapper\' -failed to load class \`FWrapper\' -failed to load class \`IWrapper\' +failed to load class \'AWrapper\' +failed to load class \'FWrapper\' +failed to load class \'IWrapper\' diff --git a/jbmc/regression/jbmc/overlay-class/correct-test.desc b/jbmc/regression/jbmc/overlay-class/correct-test.desc index ecde48e8a55..928f7a24917 100644 --- a/jbmc/regression/jbmc/overlay-class/correct-test.desc +++ b/jbmc/regression/jbmc/overlay-class/correct-test.desc @@ -1,8 +1,8 @@ CORE Test.class --classpath `../../../../scripts/format_classpath.sh . annotations correct-overlay` --verbosity 10 -^Getting class `Test' from file \.[\\/]Test\.class$ -^Getting class `Test' from file correct-overlay[\\/]Test\.class$ +^Getting class 'Test' from file \.[\\/]Test\.class$ +^Getting class 'Test' from file correct-overlay[\\/]Test\.class$ ^Adding symbol from overlay class: field 'x'$ ^Adding symbol from overlay class: method 'java::Test\.:\(\)V'$ ^Field definition for java::Test\.x already loaded from overlay class$ diff --git a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc index 2bfce7a5ca3..fd04cf072e3 100644 --- a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc +++ b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc @@ -1,8 +1,8 @@ CORE Test.class --classpath `../../../../scripts/format_classpath.sh . annotations . correct-overlay` --verbosity 10 -^Getting class `Test' from file \.[\\/]Test\.class$ -^Getting class `Test' from file correct-overlay[\\/]Test\.class$ +^Getting class 'Test' from file \.[\\/]Test\.class$ +^Getting class 'Test' from file correct-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ ^Adding symbol from overlay class: field 'x'$ ^Adding symbol from overlay class: method 'java::Test\.:\(\)V'$ diff --git a/jbmc/regression/jbmc/overlay-class/misordered-test.desc b/jbmc/regression/jbmc/overlay-class/misordered-test.desc index 6505d5449d1..4a0cd937758 100644 --- a/jbmc/regression/jbmc/overlay-class/misordered-test.desc +++ b/jbmc/regression/jbmc/overlay-class/misordered-test.desc @@ -1,8 +1,8 @@ CORE Test.class --classpath `../../../../scripts/format_classpath.sh annotations correct-overlay .` --verbosity 10 -^Getting class `Test' from file correct-overlay[\\/]Test\.class$ -^Getting class `Test' from file \.[\\/]Test\.class$ +^Getting class 'Test' from file correct-overlay[\\/]Test\.class$ +^Getting class 'Test' from file \.[\\/]Test\.class$ ^Skipping class Test marked with OverlayClassImplementation but found before original definition$ ^Adding symbol: field 'x'$ ^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$ diff --git a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc index cbf0430a3a6..46b6190c31f 100644 --- a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc +++ b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc @@ -1,8 +1,8 @@ CORE Test.class --classpath `../../../../scripts/format_classpath.sh . annotations unmarked-overlay` --verbosity 10 -^Getting class `Test' from file \.[\\/]Test\.class$ -^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$ +^Getting class 'Test' from file \.[\\/]Test\.class$ +^Getting class 'Test' from file unmarked-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ ^Adding symbol: field 'x'$ ^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$ diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 75f535cc141..8bbdd4a49c4 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -435,7 +435,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - log.error() << "Failed to open json output `" << json_file << "'" + log.error() << "Failed to open json output '" << json_file << "'" << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -461,7 +461,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - log.error() << "Failed to open json output `" << json_file << "'" + log.error() << "Failed to open json output '" << json_file << "'" << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -487,7 +487,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - log.error() << "Failed to open json output `" << json_file << "'" + log.error() << "Failed to open json output '" << json_file << "'" << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -538,7 +538,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(!out) { - log.error() << "Failed to open output file `" << outfile << "'" + log.error() << "Failed to open output file '" << outfile << "'" << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 07a245e576e..9ec97ce35d3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1889,8 +1889,8 @@ java_bytecode_parse( if(!in) { messaget message(message_handler); - message.error() << "failed to open input file `" - << file << '\'' << messaget::eom; + message.error() << "failed to open input file '" << file << '\'' + << messaget::eom; return {}; } diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index c7cd32ced40..9034345a54a 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -176,7 +176,7 @@ java_class_loadert::get_parse_tree( return parse_trees; // Not found or failed to load - warning() << "failed to load class `" << class_name << '\'' << eom; + warning() << "failed to load class \'" << class_name << '\'' << eom; parse_trees.emplace_back(class_name); return parse_trees; } @@ -211,10 +211,10 @@ java_class_loadert::read_jar_file(const std::string &jar_path) } catch(const std::runtime_error &) { - error() << "failed to open JAR file `" << jar_path << "'" << eom; + error() << "failed to open JAR file '" << jar_path << "'" << eom; return {}; } - debug() << "Adding JAR file `" << jar_path << "'" << eom; + debug() << "Adding JAR file '" << jar_path << "'" << eom; // Create a new entry in the map and initialize using the list of file names // that are in jar_filet @@ -223,9 +223,8 @@ java_class_loadert::read_jar_file(const std::string &jar_path) { if(has_suffix(file_name, ".class")) { - debug() - << "Found class file " << file_name << " in JAR `" << jar_path << "'" - << eom; + debug() << "Found class file " << file_name << " in JAR '" << jar_path + << "'" << eom; irep_idt class_name=file_to_class_name(file_name); classes.push_back(class_name); } diff --git a/jbmc/src/java_bytecode/java_class_loader_base.cpp b/jbmc/src/java_bytecode/java_class_loader_base.cpp index a3d234bb800..e81ff64cadf 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_base.cpp @@ -142,7 +142,7 @@ java_class_loader_baset::get_class_from_jar( if(!data.has_value()) return {}; - debug() << "Getting class `" << class_name << "' from JAR " << jar_file + debug() << "Getting class '" << class_name << "' from JAR " << jar_file << eom; std::istringstream istream(*data); @@ -150,7 +150,7 @@ java_class_loader_baset::get_class_from_jar( } catch(const std::runtime_error &) { - error() << "failed to open JAR file `" << jar_file << "'" << eom; + error() << "failed to open JAR file '" << jar_file << "'" << eom; return {}; } } @@ -170,7 +170,7 @@ java_class_loader_baset::get_class_from_directory( if(std::ifstream(full_path)) { - debug() << "Getting class `" << class_name << "' from file " << full_path + debug() << "Getting class '" << class_name << "' from file " << full_path << eom; return java_bytecode_parse(full_path, get_message_handler()); } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index f216ecbfebc..ebd9ffc2988 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -496,7 +496,7 @@ int jbmc_parse_optionst::doit() if(!infile) { - log.error() << "failed to open input file `" << filename << "'" + log.error() << "failed to open input file '" << filename << "'" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } @@ -506,7 +506,7 @@ int jbmc_parse_optionst::doit() if(language==nullptr) { - log.error() << "failed to figure out type of file `" << filename << "'" + log.error() << "failed to figure out type of file '" << filename << "'" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } diff --git a/regression/ansi-c/Array_Declarator8/test.desc b/regression/ansi-c/Array_Declarator8/test.desc index d42f8db33a9..c83b6fd2e70 100644 --- a/regression/ansi-c/Array_Declarator8/test.desc +++ b/regression/ansi-c/Array_Declarator8/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -array size of static symbol `B' is not constant$ +array size of static symbol 'B' is not constant$ -- ^warning: ignoring diff --git a/regression/ansi-c/linking_conflicts1/test.desc b/regression/ansi-c/linking_conflicts1/test.desc index 92ed8df59a9..73decc3320d 100644 --- a/regression/ansi-c/linking_conflicts1/test.desc +++ b/regression/ansi-c/linking_conflicts1/test.desc @@ -4,7 +4,7 @@ other.c ^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -error: conflicting function declarations `bar' -error: conflicting function declarations `bar2' +error: conflicting function declarations 'bar' +error: conflicting function declarations 'bar2' -- ^warning: ignoring diff --git a/regression/ansi-c/linking_conflicts2/test.desc b/regression/ansi-c/linking_conflicts2/test.desc index 194ffe12576..824f75300d6 100644 --- a/regression/ansi-c/linking_conflicts2/test.desc +++ b/regression/ansi-c/linking_conflicts2/test.desc @@ -4,6 +4,6 @@ other.c ^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -error: conflicting function declarations `foo' +error: conflicting function declarations 'foo' -- ^warning: ignoring diff --git a/regression/ansi-c/message_handling1/test.desc b/regression/ansi-c/message_handling1/test.desc index 908d5eb7688..14aa355de9f 100644 --- a/regression/ansi-c/message_handling1/test.desc +++ b/regression/ansi-c/message_handling1/test.desc @@ -4,4 +4,4 @@ main.c ^EXIT=0$ ^SIGNAL=0$ -- -encountered goto `bla' that enters one or more lexical blocks +encountered goto 'bla' that enters one or more lexical blocks diff --git a/regression/ansi-c/static2/test.desc b/regression/ansi-c/static2/test.desc index 7e5030c44c2..fb887e42144 100644 --- a/regression/ansi-c/static2/test.desc +++ b/regression/ansi-c/static2/test.desc @@ -1,7 +1,7 @@ CORE test-c++-front-end main.c main2.c --function foo -^main symbol `foo' is ambiguous$ +^main symbol 'foo' is ambiguous$ ^EXIT=(1|64)$ ^SIGNAL=0$ -- diff --git a/regression/ansi-c/static3/test.desc b/regression/ansi-c/static3/test.desc index 7e5030c44c2..fb887e42144 100644 --- a/regression/ansi-c/static3/test.desc +++ b/regression/ansi-c/static3/test.desc @@ -1,7 +1,7 @@ CORE test-c++-front-end main.c main2.c --function foo -^main symbol `foo' is ambiguous$ +^main symbol 'foo' is ambiguous$ ^EXIT=(1|64)$ ^SIGNAL=0$ -- diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index e9297e995aa..7dbaea9ddd6 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -3,12 +3,12 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition 'C && D && !E && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition 'C && !D && E && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition '!C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition 'C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition 'C && D && E && !A && B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition 'C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc index 87c44864772..4fcb0019b37 100644 --- a/regression/cbmc-cover/mcdc10/test.desc +++ b/regression/cbmc-cover/mcdc10/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$ -^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && !\(C != FALSE\).*: SATISFIED$ -^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE.*: SATISFIED$ -^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'A != FALSE && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition '!\(A != FALSE\) && B != FALSE && !\(C != FALSE\).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition '!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(A != FALSE\) && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc index 2027e1577be..58e30626566 100644 --- a/regression/cbmc-cover/mcdc11/test.desc +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -3,12 +3,12 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$ -^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$ -^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$ -^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$ -^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$ -^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition 'A != FALSE && B != FALSE.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition 'A != FALSE && !\(B != FALSE\).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition '!\(A != FALSE\) && B != FALSE.*: SATISFIED$ +^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition 'C != FALSE && !\(D != FALSE\).*: SATISFIED$ +^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition '!\(C != FALSE\) && D != FALSE.*: SATISFIED$ +^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition '!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc index 03a731e6d27..32f1edf3de6 100644 --- a/regression/cbmc-cover/mcdc12/test.desc +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -3,15 +3,15 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$ -^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$ -^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$ -^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$ -^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$ -^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ -^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !\(F != FALSE\).*: SATISFIED$ -^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$ -^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$ +^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition 'A != FALSE && B != FALSE.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition 'A != FALSE && !\(B != FALSE\).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition '!\(A != FALSE\) && B != FALSE.*: SATISFIED$ +^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition 'C != FALSE && !\(D != FALSE\).*: SATISFIED$ +^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition '!\(C != FALSE\) && D != FALSE.*: SATISFIED$ +^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition '!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ +^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition 'E != FALSE && !\(F != FALSE\).*: SATISFIED$ +^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition '!\(E != FALSE\) && F != FALSE.*: SATISFIED$ +^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition '!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc index e47d7569f65..d02c72f3920 100644 --- a/regression/cbmc-cover/mcdc13/test.desc +++ b/regression/cbmc-cover/mcdc13/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$ -^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !\(C != FALSE\).* SATISFIED$ -^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE.* SATISFIED$ -^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE.* SATISFIED$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'A != FALSE && B != FALSE && C != FALSE.* SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'A != FALSE && B != FALSE && !\(C != FALSE\).* SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition 'A != FALSE && !\(B != FALSE\) && C != FALSE.* SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(A != FALSE\) && B != FALSE && C != FALSE.* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc index 09cf68d35d2..febb3db25e5 100644 --- a/regression/cbmc-cover/mcdc14/test.desc +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -3,8 +3,8 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ -^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ +^\[main.coverage.1\] file main.c line 7 function main decision/condition 'altitude > 2500.* SATISFIED$ +^\[main.coverage.2\] file main.c line 7 function main decision/condition 'altitude > 2500.* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc index ad7dd7577aa..6e47d7166ea 100644 --- a/regression/cbmc-cover/mcdc2/test.desc +++ b/regression/cbmc-cover/mcdc2/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition 'A && !B && !C.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!A && B && !C.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!A && !B && C.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!A && !B && !C.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc index 396c7cd5e0d..e8e601cf0d7 100644 --- a/regression/cbmc-cover/mcdc3/test.desc +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -3,9 +3,9 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!\(x > \(unsigned int\)3\) && !\(y < \(unsigned int\)5\).*: SATISFIED$ -^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$ -^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$ +^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition '!\(x > \(unsigned int\)3\) && !\(y < \(unsigned int\)5\).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition 'y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition 'y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc index 73bc9565769..525aeba2971 100644 --- a/regression/cbmc-cover/mcdc4/test.desc +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -3,11 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition 'A && B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition 'A && !B && C && D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition 'A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition '!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition '!A && B && C && !D.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc index 571e0d094f7..b2ab21b77b0 100644 --- a/regression/cbmc-cover/mcdc5/test.desc +++ b/regression/cbmc-cover/mcdc5/test.desc @@ -3,11 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ -^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition 'A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!C && !D && A && !B.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!A && B && C && !D.*: SATISFIED$ +^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition '!A && !B && C && !D.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc index 267488742c2..d49ece1946a 100644 --- a/regression/cbmc-cover/mcdc6/test.desc +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -3,8 +3,8 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$ -^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$ +^\[main.coverage.1\] file main.c line 7 function main decision/condition 'x < \(unsigned int\)3.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 7 function main decision/condition 'x < \(unsigned int\)3.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc index c288cbab0ce..4b14fcad5df 100644 --- a/regression/cbmc-cover/mcdc7/test.desc +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 8 function main decision/condition `x \* 123 > 100.* false: SATISFIED$ -^\[main.coverage.2\] file main.c line 8 function main decision/condition `x \* 123 > 100.* true: SATISFIED$ -^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$ -^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$ +^\[main.coverage.1\] file main.c line 8 function main decision/condition 'x \* 123 > 100.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 8 function main decision/condition 'x \* 123 > 100.* true: SATISFIED$ +^\[main.coverage.3\] file main.c line 8 function main decision/condition 'x \* 123 < 0.* false: SATISFIED$ +^\[main.coverage.4\] file main.c line 8 function main decision/condition 'x \* 123 < 0.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index 43a1b2ca741..5c5bee9eaed 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$ -^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$ -^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$ -^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition 'c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition '!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index 199f3f14885..a56e7677b05 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -3,11 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ -^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE && A != FALSE && !\(B != FALSE\).* SATISFIED$ -^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\) && A != FALSE && !\(B != FALSE\).* SATISFIED$ -^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$ -^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ +^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition 'A != FALSE && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ +^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition '!\(C != FALSE\) && D != FALSE && A != FALSE && !\(B != FALSE\).* SATISFIED$ +^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition '!\(C != FALSE\) && !\(D != FALSE\) && A != FALSE && !\(B != FALSE\).* SATISFIED$ +^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition '!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$ +^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition '!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -- ^warning: ignoring diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc index 73e628e5f34..c9ede9f1fe2 100644 --- a/regression/cbmc/array-function-parameters/test.desc +++ b/regression/cbmc/array-function-parameters/test.desc @@ -14,6 +14,6 @@ test.c \[test.assertion.9\] line \d+ assertion Test.lists\[0\] != Test.lists\[1\]: SUCCESS \[test.assertion.10\] line \d+ assertion Test.lists\[1\] != Test.lists\[2\]: SUCCESS \[test.assertion.11\] line \d+ assertion Test.lists\[2\] != Test.lists\[3\]: SUCCESS -\[test.array_bounds.1\] line \d+ array `Test'.lists upper bound in Test.lists\[\(signed long( long)? int\)4\]: FAILURE +\[test.array_bounds.1\] line \d+ array 'Test'.lists upper bound in Test.lists\[\(signed long( long)? int\)4\]: FAILURE \[test.assertion.12\] line \d+ assertion !Test.lists\[4\]: FAILURE -- diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 9904cb35405..2ed565c0062 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -1,7 +1,7 @@ CORE main.c --signed-overflow-check --bounds-check -line 14 array `y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ +line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ ^\*\* 1 of 1 failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/goto-cc-file-local/name-clash-with-suffix/test.desc b/regression/goto-cc-file-local/name-clash-with-suffix/test.desc index d2fe012bcca..c9a6dff3a8c 100644 --- a/regression/goto-cc-file-local/name-clash-with-suffix/test.desc +++ b/regression/goto-cc-file-local/name-clash-with-suffix/test.desc @@ -4,7 +4,7 @@ use_find out-file-counter final-link wall suffix assertion-check ^EXIT=0$ ^SIGNAL=0$ -- -^.*warning: function `__CPROVER_file_local_main_c_static_fun' in module `main' is shadowed by a definition in module `main' +^.*warning: function '__CPROVER_file_local_main_c_static_fun' in module 'main' is shadowed by a definition in module 'main' ^warning: ignoring ^\*\*\*\* WARNING: no body for function -- diff --git a/regression/goto-cc-file-local/name-clash/test.desc b/regression/goto-cc-file-local/name-clash/test.desc index aacbe41f70f..e744cd8c121 100644 --- a/regression/goto-cc-file-local/name-clash/test.desc +++ b/regression/goto-cc-file-local/name-clash/test.desc @@ -3,7 +3,7 @@ foo/bar/baz/main.c use_find out-file-counter final-link wall ^EXIT=0$ ^SIGNAL=0$ -^.*warning: function `__CPROVER_file_local_main_c_static_fun' in module `main' is shadowed by a definition in module `main' +^.*warning: function '__CPROVER_file_local_main_c_static_fun' in module 'main' is shadowed by a definition in module 'main' -- ^warning: ignoring ^\*\*\*\* WARNING: no body for function @@ -14,7 +14,7 @@ scheme will give the static functions identical names when they get exported. This test ensures that the compiler emits a warning about this. -CBMC spins forever when run on the final object file, since the `foo' +CBMC spins forever when run on the final object file, since the 'foo' implementation of `static_fun` is the one that is kept. There is thus an infinite loop where foo/static_fun() calls bar(), and bar() calls foo/static_fun() instead of bar/static_fun(). diff --git a/regression/goto-instrument/inline_05/test.desc b/regression/goto-instrument/inline_05/test.desc index c28e702b192..4ca5a26aa86 100644 --- a/regression/goto-instrument/inline_05/test.desc +++ b/regression/goto-instrument/inline_05/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -recursion.*ignored.*[`]f -recursion.*ignored.*[`]g +recursion.*ignored.*'f +recursion.*ignored.*'g -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_06/test.desc b/regression/goto-instrument/inline_06/test.desc index 70a8f0beafa..7fc5f6eba3c 100644 --- a/regression/goto-instrument/inline_06/test.desc +++ b/regression/goto-instrument/inline_06/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -recursion.*ignored.*[`]f -recursion.*ignored.*[`]g +recursion.*ignored.*'f +recursion.*ignored.*'g -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_07/test.desc b/regression/goto-instrument/inline_07/test.desc index 94d9bb1c818..ce90ccc8b4e 100644 --- a/regression/goto-instrument/inline_07/test.desc +++ b/regression/goto-instrument/inline_07/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -recursion.*ignored.*[`]f -recursion.*ignored.*[`]g +recursion.*ignored.*'f +recursion.*ignored.*'g -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_09/test.desc b/regression/goto-instrument/inline_09/test.desc index b759f98597d..5bb9b6b5e91 100644 --- a/regression/goto-instrument/inline_09/test.desc +++ b/regression/goto-instrument/inline_09/test.desc @@ -7,7 +7,7 @@ main.c ^\s*x;$ ^\s*c;$ ^\s*a;$ -no body.*[`]f +no body.*'f -- f\(\) ^warning: ignoring diff --git a/regression/smt2_solver/function-applications/function-application2.desc b/regression/smt2_solver/function-applications/function-application2.desc index d1a337f6a9c..b9f8456d7a2 100644 --- a/regression/smt2_solver/function-applications/function-application2.desc +++ b/regression/smt2_solver/function-applications/function-application2.desc @@ -3,5 +3,5 @@ function-application2.smt2 ^EXIT=20$ ^SIGNAL=0$ -^\(error "line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'"\)$ +^\(error "line 5: type mismatch in function definition: expected '\(_ BitVec 16\)' but got '\(_ BitVec 8\)'"\)$ -- diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 7880faae78e..3cbe6a09028 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1527,7 +1527,7 @@ void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard) { INVARIANT( expr.is_boolean(), - "`" + expr.id_string() + "' must be Boolean, but got " + expr.pretty()); + "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty()); guardt old_guard = guard; @@ -1535,7 +1535,7 @@ void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard) { INVARIANT( op.is_boolean(), - "`" + expr.id_string() + "' takes Boolean operands only, but got " + + "'" + expr.id_string() + "' takes Boolean operands only, but got " + op.pretty()); check_rec(op, guard); diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 6f3a9954628..c53b33709e8 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -478,7 +478,7 @@ void rw_range_sett::get_objects_address_of(const exprt &object) get_objects_rec(get_modet::READ, address_of_exprt(tc.op())); } else - throw "rw_range_sett: address_of `"+object.id_string()+"' not handled"; + throw "rw_range_sett: address_of '" + object.id_string() + "' not handled"; } void rw_range_sett::add( @@ -595,7 +595,7 @@ void rw_range_sett::get_objects_rec( get_objects_rec(mode, *it); } else - throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; + throw "rw_range_sett: assignment to '" + expr.id_string() + "' not handled"; } void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 05426f8b5e2..d51e49d39d9 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -133,7 +133,7 @@ bool ansi_c_entry_point( if(matches.empty()) { messaget message(message_handler); - message.error() << "main symbol `" << config.main.value() << "' not found" + message.error() << "main symbol '" << config.main.value() << "' not found" << messaget::eom; return true; // give up } @@ -141,7 +141,7 @@ bool ansi_c_entry_point( if(matches.size()>=2) { messaget message(message_handler); - message.error() << "main symbol `" << config.main.value() + message.error() << "main symbol '" << config.main.value() << "' is ambiguous" << messaget::eom; return true; } @@ -164,7 +164,7 @@ bool ansi_c_entry_point( if(symbol.value.is_nil()) { messaget message(message_handler); - message.error() << "main symbol `" << id2string(main_symbol) + message.error() << "main symbol '" << id2string(main_symbol) << "' has no body" << messaget::eom; return false; // give up } diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index b12fc947763..ed26324648c 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -81,8 +81,8 @@ static bool convert( if(s_it==new_symbol_table.symbols.end()) { messaget message(message_handler); - message.error() << "failed to produce built-in symbol `" - << identifier << '\'' << messaget::eom; + message.error() << "failed to produce built-in symbol '" << identifier + << '\'' << messaget::eom; return true; } diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index aa827cf3df3..766550ffa7f 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -795,7 +795,7 @@ bool c_preprocess_none( if(!infile) { messaget message(message_handler); - message.error() << "failed to open `" << file << "'" << messaget::eom; + message.error() << "failed to open '" << file << "'" << messaget::eom; return true; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 71ac0069af6..261a6388ff4 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -39,8 +39,8 @@ void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol) if(symbol_table.move(symbol, new_symbol)) { error().source_location=symbol.location; - error() << "failed to move symbol `" << symbol.name - << "' into symbol table" << eom; + error() << "failed to move symbol '" << symbol.name << "' into symbol table" + << eom; throw 0; } } @@ -120,7 +120,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) if(old_it->second.is_type!=symbol.is_type) { error().source_location=symbol.location; - error() << "redeclaration of `" << symbol.display_name() + error() << "redeclaration of '" << symbol.display_name() << "' as a different kind of symbol" << eom; throw 0; } @@ -196,9 +196,8 @@ void c_typecheck_baset::typecheck_redefinition_type( else { error().source_location=new_symbol.location; - error() << "conflicting definition of type symbol `" - << new_symbol.display_name() - << '\'' << eom; + error() << "conflicting definition of type symbol '" + << new_symbol.display_name() << '\'' << eom; throw 0; } } @@ -221,9 +220,8 @@ void c_typecheck_baset::typecheck_redefinition_type( { // arg! new tag type error().source_location=new_symbol.location; - error() << "conflicting definition of tag symbol `" - << new_symbol.display_name() - << '\'' << eom; + error() << "conflicting definition of tag symbol '" + << new_symbol.display_name() << '\'' << eom; throw 0; } } @@ -247,8 +245,8 @@ void c_typecheck_baset::typecheck_redefinition_type( if(follow(new_symbol.type)!=follow(old_symbol.type)) { error().source_location=new_symbol.location; - error() << "type symbol `" - << new_symbol.display_name() << "' defined twice:\n" + error() << "type symbol '" << new_symbol.display_name() + << "' defined twice:\n" << "Original: " << to_string(old_symbol.type) << "\n" << " New: " << to_string(new_symbol.type) << eom; throw 0; @@ -312,8 +310,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( if(final_old.id()!=ID_code) { error().source_location=new_symbol.location; - error() << "error: function symbol `" - << new_symbol.display_name() + error() << "error: function symbol '" << new_symbol.display_name() << "' redefined with a different type:\n" << "Original: " << to_string(old_symbol.type) << "\n" << " New: " << to_string(new_symbol.type) << eom; @@ -370,7 +367,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( else { error().source_location=new_symbol.location; - error() << "function body `" << new_symbol.display_name() + error() << "function body '" << new_symbol.display_name() << "' defined twice" << eom; throw 0; } @@ -437,7 +434,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( else { error().source_location=new_symbol.location; - error() << "symbol `" << new_symbol.display_name() + error() << "symbol '" << new_symbol.display_name() << "' redefined with a different type:\n" << "Original: " << to_string(old_symbol.type) << "\n" << " New: " << to_string(new_symbol.type) << eom; @@ -475,7 +472,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( else { warning().source_location=new_symbol.value.find_source_location(); - warning() << "symbol `" << new_symbol.display_name() + warning() << "symbol '" << new_symbol.display_name() << "' already has an initial value" << eom; } } @@ -553,7 +550,7 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol) if(labels_defined.find(label.first) == labels_defined.end()) { error().source_location = label.second; - error() << "branching label `" << label.first + error() << "branching label '" << label.first << "' is not defined in function" << eom; throw 0; } diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 9e042a0bedd..47e4dea820b 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -273,7 +273,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) if(s_it==symbol_table.symbols.end()) { error().source_location = code.source_location(); - error() << "failed to find decl symbol `" << identifier + error() << "failed to find decl symbol '" << identifier << "' in symbol table" << eom; throw 0; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index abee5feca0b..612e866e117 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -344,7 +344,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) { error().source_location = op.source_location(); error() << "real part retrieval expects numerical operand, " - << "but got `" << to_string(op.type()) << "'" << eom; + << "but got '" << to_string(op.type()) << "'" << eom; throw 0; } @@ -381,7 +381,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) { error().source_location = op.source_location(); error() << "real part retrieval expects numerical operand, " - << "but got `" << to_string(op.type()) << "'" << eom; + << "but got '" << to_string(op.type()) << "'" << eom; throw 0; } @@ -588,7 +588,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) { error().source_location = expr.source_location(); error() << "offsetof of member expects struct/union type, " - << "but got `" << to_string(type) << "'" << eom; + << "but got '" << to_string(type) << "'" << eom; throw 0; } @@ -615,7 +615,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) if(!o_opt.has_value()) { error().source_location = expr.source_location(); - error() << "offsetof failed to determine offset of `" + error() << "offsetof failed to determine offset of '" << component_name << "'" << eom; throw 0; } @@ -648,7 +648,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) if(!o_opt.has_value()) { error().source_location = expr.source_location(); - error() << "offsetof failed to determine offset of `" + error() << "offsetof failed to determine offset of '" << component_name << "'" << eom; throw 0; } @@ -671,9 +671,9 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) if(!found2) { error().source_location = expr.source_location(); - error() << "offset-of of member failed to find component `" - << component_name << "' in `" - << to_string(type) << "'" << eom; + error() << "offset-of of member failed to find component '" + << component_name << "' in '" << to_string(type) << "'" + << eom; throw 0; } } @@ -762,7 +762,7 @@ 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 decl symbol `" << identifier + error() << "failed to find decl symbol '" << identifier << "' in symbol table" << eom; throw 0; } @@ -819,8 +819,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) if(lookup(identifier, symbol_ptr)) { error().source_location = expr.source_location(); - error() << "failed to find symbol `" - << identifier << "'" << eom; + error() << "failed to find symbol '" << identifier << "'" << eom; throw 0; } @@ -829,7 +828,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) if(symbol.is_type) { error().source_location = expr.source_location(); - error() << "did not expect a type symbol here, but got `" + error() << "did not expect a type symbol here, but got '" << symbol.display_name() << "'" << eom; throw 0; } @@ -1102,8 +1101,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) // not found, complain error().source_location = expr.source_location(); - error() << "type cast to union: type `" - << to_string(op.type()) << "' not found in union" << eom; + error() << "type cast to union: type '" << to_string(op.type()) + << "' not found in union" << eom; throw 0; } @@ -1158,8 +1157,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) if(!is_numeric_type(expr_type) && expr_type.id()!=ID_pointer) { error().source_location = expr.source_location(); - error() << "type cast to `" - << to_string(expr_type) << "' is not permitted" << eom; + error() << "type cast to '" << to_string(expr_type) << "' is not permitted" + << eom; throw 0; } @@ -1176,7 +1175,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) if(expr_type.id()!=ID_empty) { error().source_location = expr.source_location(); - error() << "type cast from void only permitted to void, but got `" + error() << "type cast from void only permitted to void, but got '" << to_string(expr.type()) << "'" << eom; throw 0; } @@ -1197,16 +1196,16 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) else { error().source_location = expr.source_location(); - error() << "type cast from vector to `" - << to_string(expr.type()) << "' not permitted" << eom; + error() << "type cast from vector to '" << to_string(expr.type()) + << "' not permitted" << eom; throw 0; } } else { error().source_location = expr.source_location(); - error() << "type cast from `" - << to_string(op_type) << "' not permitted" << eom; + error() << "type cast from '" << to_string(op_type) << "' not permitted" + << eom; throw 0; } @@ -1236,8 +1235,7 @@ void c_typecheck_baset::typecheck_expr_index(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -1291,7 +1289,7 @@ void c_typecheck_baset::typecheck_expr_index(exprt &expr) else { error().source_location = expr.source_location(); - error() << "operator [] must take array/vector or pointer but got `" + error() << "operator [] must take array/vector or pointer but got '" << to_string(array_expr.type()) << "'" << eom; throw 0; } @@ -1407,10 +1405,9 @@ void c_typecheck_baset::typecheck_expr_rel( } error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' not defined for types `" - << to_string(o_type0) << "' and `" - << to_string(o_type1) << "'" << eom; + error() << "operator '" << expr.id() << "' not defined for types '" + << to_string(o_type0) << "' and '" << to_string(o_type1) << "'" + << eom; throw 0; } @@ -1428,10 +1425,9 @@ void c_typecheck_baset::typecheck_expr_rel_vector( o_type0.subtype() != o_type1.subtype()) { error().source_location = expr.source_location(); - error() << "vector operator `" << expr.id() - << "' not defined for types `" - << to_string(o_type0) << "' and `" - << to_string(o_type1) << "'" << eom; + error() << "vector operator '" << expr.id() << "' not defined for types '" + << to_string(o_type0) << "' and '" << to_string(o_type1) << "'" + << eom; throw 0; } @@ -1471,7 +1467,7 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr) { error().source_location = expr.source_location(); error() << "ptrmember operator requires pointer or array type " - "on left hand side, but got `" + "on left hand side, but got '" << to_string(expr.op0().type()) << "'" << eom; throw 0; } @@ -1499,7 +1495,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr) { error().source_location = expr.source_location(); error() << "member operator requires structure type " - "on left hand side but got `" + "on left hand side but got '" << to_string(type) << "'" << eom; throw 0; } @@ -1532,8 +1528,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr) { // give up error().source_location = expr.source_location(); - error() << "member `" << component_name - << "' not found in `" + error() << "member '" << component_name << "' not found in '" << to_string(type) << "'" << eom; throw 0; } @@ -1562,8 +1557,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr) if(access==ID_private) { error().source_location = expr.source_location(); - error() << "member `" << component_name - << "' is " << access << eom; + error() << "member '" << component_name << "' is " << access << eom; throw 0; } } @@ -1654,9 +1648,8 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr) } error().source_location = expr.source_location(); - error() << "operator ?: not defined for types `" - << to_string(o_type1) << "' and `" - << to_string(o_type2) << "'" << eom; + error() << "operator ?: not defined for types '" << to_string(o_type1) + << "' and '" << to_string(o_type2) << "'" << eom; throw 0; } @@ -1757,8 +1750,8 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr) else { error().source_location = expr.source_location(); - error() << "address_of error: `" << to_string(op) - << "' not an lvalue" << eom; + error() << "address_of error: '" << to_string(op) << "' not an lvalue" + << eom; throw 0; } @@ -1793,9 +1786,9 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr) else { error().source_location = expr.source_location(); - error() << "operand of unary * `" << to_string(op) - << "' is not a pointer, but got `" - << to_string(op_type) << "'" << eom; + error() << "operand of unary * '" << to_string(op) + << "' is not a pointer, but got '" << to_string(op_type) << "'" + << eom; throw 0; } @@ -1840,7 +1833,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) if(!op0.get_bool(ID_C_lvalue)) { error().source_location = op0.source_location(); - error() << "prefix operator error: `" << to_string(op0) + error() << "prefix operator error: '" << to_string(op0) << "' not an lvalue" << eom; throw 0; } @@ -1848,8 +1841,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) if(type0.get_bool(ID_C_constant)) { error().source_location = op0.source_location(); - error() << "error: `" << to_string(op0) - << "' is constant" << eom; + error() << "error: '" << to_string(op0) << "' is constant" << eom; throw 0; } @@ -1859,8 +1851,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) if(enum_type.is_incomplete()) { error().source_location = expr.source_location(); - error() << "operator `" << statement - << "' given incomplete type `" + error() << "operator '" << statement << "' given incomplete type '" << to_string(type0) << "'" << eom; throw 0; } @@ -1893,8 +1884,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) else { error().source_location = expr.source_location(); - error() << "operator `" << statement - << "' not defined for type `" + error() << "operator '" << statement << "' not defined for type '" << to_string(type0) << "'" << eom; throw 0; } @@ -2045,7 +2035,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( move_symbol(new_symbol, symbol_ptr); warning().source_location=f_op.find_source_location(); - warning() << "function `" << identifier << "' is not declared" << eom; + warning() << "function '" << identifier << "' is not declared" << eom; } } } @@ -2058,7 +2048,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(f_op_type.id()!=ID_pointer) { error().source_location = f_op.source_location(); - error() << "expected function/function pointer as argument but got `" + error() << "expected function/function pointer as argument but got '" << to_string(f_op_type) << "'" << eom; throw 0; } @@ -2970,8 +2960,7 @@ void c_typecheck_baset::typecheck_expr_unary_arithmetic(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects one operand" << eom; + error() << "operator '" << expr.id() << "' expects one operand" << eom; throw 0; } @@ -2998,8 +2987,7 @@ void c_typecheck_baset::typecheck_expr_unary_arithmetic(exprt &expr) } error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' not defined for type `" + error() << "operator '" << expr.id() << "' not defined for type '" << to_string(operand.type()) << "'" << eom; throw 0; } @@ -3009,8 +2997,7 @@ void c_typecheck_baset::typecheck_expr_unary_boolean(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects one operand" << eom; + error() << "operator '" << expr.id() << "' expects one operand" << eom; throw 0; } @@ -3059,8 +3046,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -3168,10 +3154,9 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr) } error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' not defined for types `" - << to_string(o_type0) << "' and `" - << to_string(o_type1) << "'" << eom; + error() << "operator '" << expr.id() << "' not defined for types '" + << to_string(o_type0) << "' and '" << to_string(o_type1) << "'" + << eom; throw 0; } @@ -3236,10 +3221,9 @@ void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr) } error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' not defined for types `" - << to_string(o_type0) << "' and `" - << to_string(o_type1) << "'" << eom; + error() << "operator '" << expr.id() << "' not defined for types '" + << to_string(o_type0) << "' and '" << to_string(o_type1) << "'" + << eom; throw 0; } @@ -3351,10 +3335,8 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr) op_name=expr.id(); error().source_location = expr.source_location(); - error() << "operator `" << op_name - << "' not defined for types `" - << to_string(type0) << "' and `" - << to_string(type1) << "'" << eom; + error() << "operator '" << op_name << "' not defined for types '" + << to_string(type0) << "' and '" << to_string(type1) << "'" << eom; throw 0; } @@ -3363,8 +3345,7 @@ void c_typecheck_baset::typecheck_expr_binary_boolean(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -3385,8 +3366,8 @@ void c_typecheck_baset::typecheck_side_effect_assignment( if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.get_statement() - << "' expects two operands" << eom; + error() << "operator '" << expr.get_statement() << "' expects two operands" + << eom; throw 0; } @@ -3408,16 +3389,15 @@ void c_typecheck_baset::typecheck_side_effect_assignment( if(!op0.get_bool(ID_C_lvalue)) { error().source_location = expr.source_location(); - error() << "assignment error: `" << to_string(op0) - << "' not an lvalue" << eom; + error() << "assignment error: '" << to_string(op0) << "' not an lvalue" + << eom; throw 0; } if(type0.get_bool(ID_C_constant)) { error().source_location = expr.source_location(); - error() << "`" << to_string(op0) - << "' is constant" << eom; + error() << "'" << to_string(op0) << "' is constant" << eom; throw 0; } @@ -3556,10 +3536,9 @@ void c_typecheck_baset::typecheck_side_effect_assignment( } error().source_location = expr.source_location(); - error() << "assignment `" << statement - << "' not defined for types `" - << to_string(o_type0) << "' and `" - << to_string(o_type1) << "'" << eom; + error() << "assignment '" << statement << "' not defined for types '" + << to_string(o_type0) << "' and '" << to_string(o_type1) << "'" + << eom; throw 0; } @@ -3579,8 +3558,8 @@ void c_typecheck_baset::make_constant(exprt &expr) expr.id()!=ID_infinity) { error().source_location=expr.find_source_location(); - error() << "expected constant expression, but got `" - << to_string(expr) << "'" << eom; + error() << "expected constant expression, but got '" << to_string(expr) + << "'" << eom; throw 0; } } diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 9d77a6b1951..a7f37854b2a 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -62,7 +62,7 @@ exprt c_typecheck_baset::do_initializer_rec( to_struct_union_type(full_type).is_incomplete()) { error().source_location = value.source_location(); - error() << "type `" << to_string(type) + error() << "type '" << to_string(type) << "' is still incomplete -- cannot initialize" << eom; throw 0; } @@ -122,7 +122,7 @@ exprt c_typecheck_baset::do_initializer_rec( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize array with subtype `" + error() << "cannot zero-initialize array with subtype '" << to_string(full_type.subtype()) << "'" << eom; throw 0; } @@ -184,7 +184,7 @@ exprt c_typecheck_baset::do_initializer_rec( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize array with subtype `" + error() << "cannot zero-initialize array with subtype '" << to_string(full_type.subtype()) << "'" << eom; throw 0; } @@ -199,18 +199,17 @@ exprt c_typecheck_baset::do_initializer_rec( to_array_type(full_type).size().is_nil()) { error().source_location = value.source_location(); - error() << "type `" << to_string(full_type) - << "' cannot be initialized with `" << to_string(value) - << "'" << eom; + error() << "type '" << to_string(full_type) + << "' cannot be initialized with '" << to_string(value) << "'" + << eom; throw 0; } if(value.id()==ID_designated_initializer) { error().source_location = value.source_location(); - error() << "type `" << to_string(full_type) - << "' cannot be initialized with designated initializer" - << eom; + error() << "type '" << to_string(full_type) + << "' cannot be initialized with designated initializer" << eom; throw 0; } @@ -324,7 +323,7 @@ void c_typecheck_baset::designator_enter( if(!array_size.has_value()) { error().source_location = array_type.size().source_location(); - error() << "array has non-constant size `" + error() << "array has non-constant size '" << to_string(array_type.size()) << "'" << eom; throw 0; } @@ -342,7 +341,7 @@ void c_typecheck_baset::designator_enter( if(!vector_size.has_value()) { error().source_location = vector_type.size().source_location(); - error() << "vector has non-constant size `" + error() << "vector has non-constant size '" << to_string(vector_type.size()) << "'" << eom; throw 0; } @@ -410,7 +409,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize array with subtype `" + error() << "cannot zero-initialize array with subtype '" << to_string(full_type.subtype()) << "'" << eom; throw 0; } @@ -480,7 +479,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize union component of type `" + error() << "cannot zero-initialize union component of type '" << to_string(component.type()) << "'" << eom; throw 0; } @@ -544,7 +543,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize union component of type `" + error() << "cannot zero-initialize union component of type '" << to_string(component.type()) << "'" << eom; throw 0; } @@ -626,9 +625,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( else { error().source_location = value.source_location(); - error() << "cannot initialize type `" - << to_string(dest_type) << "' using value `" - << to_string(value) << "'" << eom; + error() << "cannot initialize type '" << to_string(dest_type) + << "' using value '" << to_string(value) << "'" << eom; throw 0; } } @@ -820,9 +818,9 @@ designatort c_typecheck_baset::make_designator( if(!found) { error().source_location = d_op.source_location(); - error() << "failed to find struct component `" - << component_name << "' in initialization of `" - << to_string(struct_union_type) << "'" << eom; + error() << "failed to find struct component '" << component_name + << "' in initialization of '" << to_string(struct_union_type) + << "'" << eom; throw 0; } } @@ -830,7 +828,7 @@ designatort c_typecheck_baset::make_designator( else { error().source_location = d_op.source_location(); - error() << "designated initializers cannot initialize `" + error() << "designated initializers cannot initialize '" << to_string(full_type) << "'" << eom; throw 0; } @@ -863,7 +861,7 @@ exprt c_typecheck_baset::do_initializer_list( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize `" << to_string(full_type) << "'" + error() << "cannot zero-initialize '" << to_string(full_type) << "'" << eom; throw 0; } @@ -884,7 +882,7 @@ exprt c_typecheck_baset::do_initializer_list( if(!zero.has_value()) { error().source_location = value.source_location(); - error() << "cannot zero-initialize `" << to_string(full_type) << "'" + error() << "cannot zero-initialize '" << to_string(full_type) << "'" << eom; throw 0; } @@ -918,7 +916,7 @@ exprt c_typecheck_baset::do_initializer_list( return do_initializer_rec(value.op0(), type, force_constant); error().source_location = value.source_location(); - error() << "cannot initialize `" << to_string(full_type) + error() << "cannot initialize '" << to_string(full_type) << "' with an initializer list" << eom; throw 0; } diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 14862c7f6b8..f595574aa6a 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -297,8 +297,8 @@ void c_typecheck_baset::typecheck_type(typet &type) else { error().source_location=type.source_location(); - error() << "attribute mode `" << gcc_attr_mode - << "' applied to inappropriate type `" << to_string(type) << "'" + error() << "attribute mode '" << gcc_attr_mode + << "' applied to inappropriate type '" << to_string(type) << "'" << eom; throw 0; } @@ -613,8 +613,8 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) if(current_symbol.is_static_lifetime) { error().source_location=current_symbol.location; - error() << "array size of static symbol `" - << current_symbol.base_name << "' is not constant" << eom; + error() << "array size of static symbol '" << current_symbol.base_name + << "' is not constant" << eom; throw 0; } @@ -701,7 +701,7 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) if(!sub_size_expr_opt.has_value()) { error().source_location = source_location; - error() << "failed to determine size of vector base type `" + error() << "failed to determine size of vector base type '" << to_string(subtype) << "'" << eom; throw 0; } @@ -713,7 +713,7 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) if(!sub_size.has_value()) { error().source_location=source_location; - error() << "failed to determine size of vector base type `" + error() << "failed to determine size of vector base type '" << to_string(subtype) << "'" << eom; throw 0; } @@ -721,7 +721,7 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) if(*sub_size == 0) { error().source_location=source_location; - error() << "type had size 0: `" << to_string(subtype) << "'" << eom; + error() << "type had size 0: '" << to_string(subtype) << "'" << eom; throw 0; } @@ -847,8 +847,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) else if(have_body) { error().source_location=type.source_location(); - error() << "redefinition of body of `" - << s_it->second.pretty_name << "'" << eom; + error() << "redefinition of body of '" << s_it->second.pretty_name + << "'" << eom; throw 0; } } @@ -1507,7 +1507,7 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type) if(s_it == symbol_table.symbols.end()) { error().source_location = type.source_location(); - error() << "typedef symbol `" << identifier << "' not found" << eom; + error() << "typedef symbol '" << identifier << "' not found" << eom; throw 0; } diff --git a/src/ansi-c/c_typecheck_typecast.cpp b/src/ansi-c/c_typecheck_typecast.cpp index 09c3f055b96..38fef6120bb 100644 --- a/src/ansi-c/c_typecheck_typecast.cpp +++ b/src/ansi-c/c_typecheck_typecast.cpp @@ -23,8 +23,8 @@ void c_typecheck_baset::implicit_typecast( for(const auto &tc_error : c_typecast.errors) { error().source_location=expr.find_source_location(); - error() << "in expression `" << to_string(expr) << "':\n" - << "conversion from `" << to_string(src_type) << "' to `" + error() << "in expression '" << to_string(expr) << "':\n" + << "conversion from '" << to_string(src_type) << "' to '" << to_string(dest_type) << "': " << tc_error << eom; } @@ -34,7 +34,7 @@ void c_typecheck_baset::implicit_typecast( for(const auto &tc_warning : c_typecast.warnings) { warning().source_location=expr.find_source_location(); - warning() << "warning: conversion from `" << to_string(src_type) << "' to `" + warning() << "warning: conversion from '" << to_string(src_type) << "' to '" << to_string(dest_type) << "': " << tc_warning << eom; } } diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp index f04f955466f..e77636c5fc2 100644 --- a/src/ansi-c/literals/convert_string_literal.cpp +++ b/src/ansi-c/literals/convert_string_literal.cpp @@ -94,7 +94,7 @@ exprt convert_string_literal(const std::string &src) // find start of sequence std::size_t j=src.find('"', i); if(j==std::string::npos) - throw "invalid string constant `"+src+"'"; + throw "invalid string constant '" + src + "'"; // find end of sequence, considering escaping for(++j; j tmp_value= diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a978de62730..2c74dd4a826 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -530,7 +530,7 @@ int cbmc_parse_optionst::doit() if(!infile) { - log.error() << "failed to open input file `" << filename << "'" + log.error() << "failed to open input file '" << filename << "'" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } @@ -540,7 +540,7 @@ int cbmc_parse_optionst::doit() if(language==nullptr) { - log.error() << "failed to figure out type of file `" << filename << "'" + log.error() << "failed to figure out type of file '" << filename << "'" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 124ad9fb58b..71c77c0fa00 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -71,8 +71,8 @@ optionalt cpp_typecheckt::cpp_constructor( if(to_integer(to_constant_expr(tmp_size), s)) { error().source_location=source_location; - error() << "array size `" << to_string(size_expr) - << "' is not a constant" << eom; + error() << "array size '" << to_string(size_expr) << "' is not a constant" + << eom; throw 0; } diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index ce843c7b5ea..48f8629e34b 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -147,10 +147,9 @@ symbolt &cpp_declarator_convertert::convert( { cpp_typecheck.error().source_location= declarator.name().source_location(); - cpp_typecheck.error() << "member `" << base_name - << "' not found in scope `" - << scope->identifier << "'" - << messaget::eom; + cpp_typecheck.error() + << "member '" << base_name << "' not found in scope '" + << scope->identifier << "'" << messaget::eom; throw 0; } } @@ -285,16 +284,14 @@ void cpp_declarator_convertert::combine_types( if(i != 0 || !symbol_code_type.get_bool(ID_C_is_virtual)) { cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "symbol `" << symbol.display_name() - << "': parameter " << (i+1) - << " type mismatch\n" - << "previous type: " - << cpp_typecheck.to_string( - symbol_parameter.type()) - << "\nnew type: " - << cpp_typecheck.to_string( - decl_parameter.type()) - << messaget::eom; + cpp_typecheck.error() + << "symbol '" << symbol.display_name() << "': parameter " + << (i + 1) << " type mismatch\n" + << "previous type: " + << cpp_typecheck.to_string(symbol_parameter.type()) + << "\nnew type: " + << cpp_typecheck.to_string(decl_parameter.type()) + << messaget::eom; throw 0; } } @@ -325,12 +322,10 @@ void cpp_declarator_convertert::combine_types( } cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "symbol `" << symbol.display_name() + cpp_typecheck.error() << "symbol '" << symbol.display_name() << "' already declared with different type:\n" - << "original: " - << cpp_typecheck.to_string(symbol.type) - << "\n new: " - << cpp_typecheck.to_string(final_type) + << "original: " << cpp_typecheck.to_string(symbol.type) + << "\n new: " << cpp_typecheck.to_string(final_type) << messaget::eom; throw 0; } @@ -380,13 +375,13 @@ void cpp_declarator_convertert::handle_initializer( if(is_code) { - cpp_typecheck.error() << "body of function `" + cpp_typecheck.error() << "body of function '" << symbol.display_name() << "' has already been defined" << messaget::eom; } else { - cpp_typecheck.error() << "symbol `" + cpp_typecheck.error() << "symbol '" << symbol.display_name() << "' already has an initializer" << messaget::eom; } @@ -533,9 +528,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( if(!id.is_class() && !id.is_enum()) { cpp_typecheck.error().source_location=new_symbol->location; - cpp_typecheck.error() << "`" << base_name - << "' already in scope" - << messaget::eom; + cpp_typecheck.error() + << "'" << base_name << "' already in scope" << messaget::eom; throw 0; } } diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index f375cbe0814..f1b985bc1f0 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -45,8 +45,8 @@ optionalt cpp_typecheckt::cpp_destructor( if(to_integer(to_constant_expr(tmp_size), s)) { error().source_location=source_location; - error() << "array size `" << to_string(size_expr) - << "' is not a constant" << eom; + error() << "array size '" << to_string(size_expr) << "' is not a constant" + << eom; throw 0; } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index dee01cd33f7..1af0f1a13fe 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -77,8 +77,7 @@ std::string cpp_typecheckt::template_suffix( { error().source_location = expr.find_source_location(); error() << "template argument expression expected to be " - << "scalar constant, but got `" - << to_string(e) << "'" << eom; + << "scalar constant, but got '" << to_string(e) << "'" << eom; throw 0; } @@ -96,7 +95,7 @@ void cpp_typecheckt::show_instantiation_stack(std::ostream &out) for(const auto &e : instantiation_stack) { const symbolt &symbol = lookup(e.identifier); - out << "instantiating `" << symbol.pretty_name << "' with <"; + out << "instantiating '" << symbol.pretty_name << "' with <"; forall_expr(a_it, e.full_template_args.arguments()) { @@ -160,9 +159,8 @@ const symbolt &cpp_typecheckt::class_template_symbol( if(full_template_args.arguments().empty()) { error().source_location=source_location; - error() << "`" << template_symbol.base_name - << "' is a template; thus, expected template arguments" - << eom; + error() << "'" << template_symbol.base_name + << "' is a template; thus, expected template arguments" << eom; throw 0; } @@ -307,9 +305,8 @@ const symbolt &cpp_typecheckt::instantiate_template( if(full_template_args.arguments().empty()) { error().source_location=source_location; - error() << "`" << template_symbol.base_name - << "' is a template; thus, expected template arguments" - << eom; + error() << "'" << template_symbol.base_name + << "' is a template; thus, expected template arguments" << eom; throw 0; } diff --git a/src/cpp/cpp_scopes.h b/src/cpp/cpp_scopes.h index 55c098d0c64..5fd61da9286 100644 --- a/src/cpp/cpp_scopes.h +++ b/src/cpp/cpp_scopes.h @@ -74,7 +74,7 @@ class cpp_scopest { id_mapt::const_iterator it=id_map.find(identifier); if(it==id_map.end()) - throw "id `"+id2string(identifier)+"' not found"; + throw "id '" + id2string(identifier) + "' not found"; return *(it->second); } diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp index c0cb37e4d8c..5992ef58c68 100644 --- a/src/cpp/cpp_typecheck_bases.cpp +++ b/src/cpp/cpp_typecheck_bases.cpp @@ -56,7 +56,7 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) if(base_symbol.type.id() != ID_struct) { error().source_location=name.source_location(); - error() << "expected struct or class as base, but got `" + error() << "expected struct or class as base, but got '" << to_string(base_symbol.type) << "'" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index b6f7401f421..cc4144682aa 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -270,7 +270,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) { #if 0 error().source_location=code.source_location()); - str << "error: constructor of `" + str << "error: constructor of '" << to_string(symbol_expr) << "' is not accessible"; throw 0; @@ -335,7 +335,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) if(code.operands().size()!= 1) { error().source_location=code.find_source_location(); - error() << " reference `" << to_string(symbol_expr) + error() << " reference '" << to_string(symbol_expr) << "' expects one initializer" << eom; throw 0; } @@ -377,8 +377,8 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) else { error().source_location=code.find_source_location(); - error() << "invalid member initializer `" - << to_string(symbol_expr) << "'" << eom; + error() << "invalid member initializer '" << to_string(symbol_expr) << "'" + << eom; throw 0; } } diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 8507eca3b04..c4309c77629 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -205,10 +205,10 @@ void cpp_typecheckt::typecheck_compound_type( else { error().source_location=type.source_location(); - error() << "error: compound tag `" << base_name + error() << "error: compound tag '" << base_name << "' declared previously\n" - << "location of previous definition: " - << symbol.location << eom; + << "location of previous definition: " << symbol.location + << eom; throw 0; } } @@ -721,8 +721,7 @@ void cpp_typecheckt::typecheck_compound_declarator( if(symbol_table.move(static_symbol, new_symbol)) { error().source_location=cpp_name.source_location(); - error() << "redeclaration of static member `" - << static_symbol.base_name + error() << "redeclaration of static member '" << static_symbol.base_name << "'" << eom; throw 0; } @@ -836,8 +835,7 @@ void cpp_typecheckt::put_compound_into_scope( if(!id.is_class() && !id.is_enum()) { error().source_location=compound.source_location(); - error() << "`" << base_name - << "' already in compound scope" << eom; + error() << "'" << base_name << "' already in compound scope" << eom; throw 0; } } @@ -1382,7 +1380,7 @@ void cpp_typecheckt::add_anonymous_members_to_scope( if(comp.type().id()==ID_code) { error().source_location=struct_union_symbol.type.source_location(); - error() << "anonymous struct/union member `" + error() << "anonymous struct/union member '" << struct_union_symbol.base_name << "' shall not have function members" << eom; throw 0; @@ -1401,7 +1399,7 @@ void cpp_typecheckt::add_anonymous_members_to_scope( if(cpp_scopes.current_scope().contains(base_name)) { error().source_location=comp.source_location(); - error() << "`" << base_name << "' already in scope" << eom; + error() << "'" << base_name << "' already in scope" << eom; throw 0; } @@ -1504,7 +1502,7 @@ bool cpp_typecheckt::get_component( else { error().source_location=source_location; - error() << "error: member `" << component_name + error() << "error: member '" << component_name << "' is not accessible (" << component.get(ID_access) << ")" << eom; throw 0; @@ -1540,7 +1538,7 @@ bool cpp_typecheckt::get_component( if(check_component_access(component, final_type)) { error().source_location=source_location; - error() << "error: member `" << component_name + error() << "error: member '" << component_name << "' is not accessible" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index c290ec47863..d642c56e322 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -453,8 +453,8 @@ void cpp_typecheckt::check_member_initializers( if(!ok) { error().source_location=member_name.source_location(); - error() << "invalid initializer `" << member_name.to_string() - << "'" << eom; + error() << "invalid initializer '" << member_name.to_string() << "'" + << eom; throw 0; } return; @@ -527,7 +527,7 @@ void cpp_typecheckt::check_member_initializers( if(!ok) { error().source_location=member_name.source_location(); - error() << "invalid initializer `" << base_name << "'" << eom; + error() << "invalid initializer '" << base_name << "'" << eom; throw 0; } } diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index e574572dbd3..d17860ffbeb 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -1491,13 +1491,12 @@ void cpp_typecheckt::implicit_typecast(exprt &expr, const typet &type) { show_instantiation_stack(error()); error().source_location=e.find_source_location(); - error() << "invalid implicit conversion from `" - << to_string(e.type()) << "' to `" - << to_string(type) << "'" << eom; - #if 0 + error() << "invalid implicit conversion from '" << to_string(e.type()) + << "' to '" << to_string(type) << "'" << eom; +#if 0 str << "\n " << follow(e.type()).pretty() << '\n'; str << "\n " << type.pretty() << '\n'; - #endif +#endif throw 0; } } diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 47b8da59f60..5fbbe3ea60c 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -65,7 +65,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration) if(c.type().id() == ID_code) { error().source_location=union_symbol.type.source_location(); - error() << "anonymous union `" << union_symbol.base_name + error() << "anonymous union '" << union_symbol.base_name << "' shall not have function members" << eom; throw 0; } @@ -75,8 +75,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration) if(cpp_scopes.current_scope().contains(base_name)) { error().source_location=union_symbol.type.source_location(); - error() << "identifier `" << base_name << "' already in scope" - << eom; + error() << "identifier '" << base_name << "' already in scope" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 22331739f12..2baa954307a 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -135,10 +135,9 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) if(has_body) { error().source_location=type.source_location(); - error() << "error: enum symbol `" << base_name + error() << "error: enum symbol '" << base_name << "' declared previously\n" - << "location of previous definition: " - << symbol.location << eom; + << "location of previous definition: " << symbol.location << eom; throw 0; } } @@ -209,8 +208,8 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) else { error().source_location=type.source_location(); - error() << "use of enum `" << base_name - << "' without previous declaration" << eom; + error() << "use of enum '" << base_name << "' without previous declaration" + << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 0a28a5111f7..b4e6f1d96d3 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -269,9 +269,8 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr) { error().source_location=expr.find_source_location(); error() << "error: types are incompatible.\n" - << "I got `" << type2cpp(expr.op1().type(), *this) - << "' and `" << type2cpp(expr.op2().type(), *this) - << "'." << eom; + << "I got '" << type2cpp(expr.op1().type(), *this) << "' and '" + << type2cpp(expr.op2().type(), *this) << "'." << eom; throw 0; } } @@ -850,7 +849,7 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr) if(!new_expr.has_value()) { error().source_location = expr.find_source_location(); - error() << "cannot zero-initialize `" << to_string(expr.type()) << "'" + error() << "cannot zero-initialize '" << to_string(expr.type()) << "'" << eom; throw 0; } @@ -930,10 +929,8 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr) { error().source_location=expr.find_source_location(); error() << "invalid explicit cast:\n" - << "operand type: `" << to_string(expr.op0().type()) - << "'\n" - << "casting to: `" << to_string(expr.type()) << "'" - << eom; + << "operand type: '" << to_string(expr.op0().type()) << "'\n" + << "casting to: '" << to_string(expr.type()) << "'" << eom; throw 0; } } @@ -1010,7 +1007,7 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr) if(pointer_type.id()!=ID_pointer) { error().source_location=expr.find_source_location(); - error() << "delete takes a pointer type operand, but got `" + error() << "delete takes a pointer type operand, but got '" << to_string(pointer_type) << "'" << eom; throw 0; } @@ -1091,8 +1088,8 @@ void cpp_typecheckt::typecheck_expr_member( { error().source_location=expr.find_source_location(); error() << "error: member operator requires struct/union type " - << "on left hand side but got `" - << to_string(followed_op0_type) << "'" << eom; + << "on left hand side but got '" << to_string(followed_op0_type) + << "'" << eom; throw 0; } @@ -1149,7 +1146,7 @@ void cpp_typecheckt::typecheck_expr_member( to_code_type(symbol_expr.type()).return_type().id() == ID_constructor) { error().source_location=expr.find_source_location(); - error() << "error: member `" + error() << "error: member '" << lookup(symbol_expr.get(ID_identifier)).base_name << "' is a constructor" << eom; throw 0; @@ -1163,9 +1160,9 @@ void cpp_typecheckt::typecheck_expr_member( if(pcomp.is_nil()) { error().source_location=expr.find_source_location(); - error() << "error: `" << symbol_expr.get(ID_identifier) + error() << "error: '" << symbol_expr.get(ID_identifier) << "' is not static member " - << "of class `" << to_string(op0.type()) << "'" << eom; + << "of class '" << to_string(op0.type()) << "'" << eom; throw 0; } } @@ -1209,9 +1206,8 @@ void cpp_typecheckt::typecheck_expr_member( else { error().source_location=expr.find_source_location(); - error() << "error: member `" << component_name - << "' of `" << to_string(type) - << "' not found" << eom; + error() << "error: member '" << component_name << "' of '" + << to_string(type) << "' not found" << eom; throw 0; } @@ -1250,8 +1246,8 @@ void cpp_typecheckt::typecheck_expr_ptrmember( { error().source_location=expr.find_source_location(); error() << "error: ptrmember operator requires pointer type " - << "on left hand side, but got `" - << to_string(expr.op0().type()) << "'" << eom; + << "on left hand side, but got '" << to_string(expr.op0().type()) + << "'" << eom; throw 0; } @@ -1329,9 +1325,8 @@ void cpp_typecheckt::typecheck_cast_expr(exprt &expr) { error().source_location=cast_op.find_source_location(); error() << "type mismatch on const_cast:\n" - << "operand type: `" << to_string(cast_op.type()) - << "'\n" - << "cast type: `" << to_string(type) << "'" << eom; + << "operand type: '" << to_string(cast_op.type()) << "'\n" + << "cast type: '" << to_string(type) << "'" << eom; throw 0; } } @@ -1341,9 +1336,8 @@ void cpp_typecheckt::typecheck_cast_expr(exprt &expr) { error().source_location=cast_op.find_source_location(); error() << "type mismatch on dynamic_cast:\n" - << "operand type: `" << to_string(cast_op.type()) - << "'\n" - << "cast type: `" << to_string(type) << "'" << eom; + << "operand type: '" << to_string(cast_op.type()) << "'\n" + << "cast type: '" << to_string(type) << "'" << eom; throw 0; } } @@ -1353,9 +1347,8 @@ void cpp_typecheckt::typecheck_cast_expr(exprt &expr) { error().source_location=cast_op.find_source_location(); error() << "type mismatch on reinterpret_cast:\n" - << "operand type: `" << to_string(cast_op.type()) - << "'\n" - << "cast type: `" << to_string(type) << "'" << eom; + << "operand type: '" << to_string(cast_op.type()) << "'\n" + << "cast type: '" << to_string(type) << "'" << eom; throw 0; } } @@ -1365,9 +1358,8 @@ void cpp_typecheckt::typecheck_cast_expr(exprt &expr) { error().source_location=cast_op.find_source_location(); error() << "type mismatch on static_cast:\n" - << "operand type: `" << to_string(cast_op.type()) - << "'\n" - << "cast type: `" << to_string(type) << "'" << eom; + << "operand type: '" << to_string(cast_op.type()) << "'\n" + << "cast type: '" << to_string(type) << "'" << eom; throw 0; } } @@ -1705,8 +1697,8 @@ void cpp_typecheckt::typecheck_side_effect_function_call( { error().source_location=expr.function().find_source_location(); error() << "function call expects function or function " - << "pointer as argument, but got `" - << to_string(expr.op0().type()) << "'" << eom; + << "pointer as argument, but got '" << to_string(expr.op0().type()) + << "'" << eom; throw 0; } @@ -2060,7 +2052,7 @@ void cpp_typecheckt::typecheck_side_effect_assignment(side_effect_exprt &expr) else { error().source_location=expr.find_source_location(); - error() << "bad assignment operator `" << statement << "'" << eom; + error() << "bad assignment operator '" << statement << "'" << eom; throw 0; } @@ -2127,9 +2119,8 @@ void cpp_typecheckt::typecheck_side_effect_inc_dec( else { error().source_location=expr.find_source_location(); - error() << "bad assignment operator `" - << expr.get_statement() - << "'" << eom; + error() << "bad assignment operator '" << expr.get_statement() << "'" + << eom; throw 0; } @@ -2333,8 +2324,7 @@ void cpp_typecheckt::typecheck_expr_binary_arithmetic(exprt &expr) if(expr.operands().size()!=2) { error().source_location=expr.find_source_location(); - error() << "operator `" << expr.id() << "' expects two operands" - << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 5c6c936a5e7..8ab4510a7ba 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -31,8 +31,8 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) if(symbol.value.id()!=ID_type) { error().source_location=symbol.location; - error() << "expected type as initializer for `" - << symbol.base_name << "'" << eom; + error() << "expected type as initializer for '" << symbol.base_name << "'" + << eom; throw 0; } @@ -48,9 +48,8 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) if(is_reference(symbol.type)) { error().source_location=symbol.location; - error() << "`" << symbol.base_name - << "' is declared as reference but is not initialized" - << eom; + error() << "'" << symbol.base_name + << "' is declared as reference but is not initialized" << eom; throw 0; } @@ -128,9 +127,8 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) if(symbol.type != symbol.value.type()) { error().source_location=symbol.location; - error() << "conversion from `" - << to_string(symbol.value.type()) << "' to `" - << to_string(symbol.type) << "' " << eom; + error() << "conversion from '" << to_string(symbol.value.type()) + << "' to '" << to_string(symbol.type) << "' " << eom; throw 0; } @@ -317,7 +315,7 @@ void cpp_typecheckt::zero_initializer( if(!value.has_value()) { error().source_location = source_location; - error() << "cannot zero-initialize `" << to_string(final_type) << "'" + error() << "cannot zero-initialize '" << to_string(final_type) << "'" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index 082be2f2961..10e8dcfd93a 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -41,20 +41,18 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) if(namespace_spec.alias().is_not_nil()) { error().source_location=namespace_spec.source_location(); - error() << "namespace alias `" << final_name - << "' previously declared\n" - << "location of previous declaration: " - << it->second.location << eom; + error() << "namespace alias '" << final_name << "' previously declared\n" + << "location of previous declaration: " << it->second.location + << eom; throw 0; } if(it->second.type.id()!=ID_namespace) { error().source_location=namespace_spec.source_location(); - error() << "namespace `" << final_name - << "' previously declared\n" - << "location of previous declaration: " - << it->second.location << eom; + error() << "namespace '" << final_name << "' previously declared\n" + << "location of previous declaration: " << it->second.location + << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index cbbeb9b89f7..9b2dd7c7daf 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -923,17 +923,16 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope( { cpp_typecheck.show_instantiation_stack(cpp_typecheck.error()); cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "scope `" << final_base_name - << "' not found" << messaget::eom; + cpp_typecheck.error() + << "scope '" << final_base_name << "' not found" << messaget::eom; throw 0; } else if(id_set.size()>=2) { cpp_typecheck.show_instantiation_stack(cpp_typecheck.error()); cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "scope `" - << final_base_name << "' is ambiguous" - << messaget::eom; + cpp_typecheck.error() << "scope '" << final_base_name + << "' is ambiguous" << messaget::eom; throw 0; } @@ -995,8 +994,8 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( { cpp_typecheck.show_instantiation_stack(cpp_typecheck.error()); cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "template scope `" << base_name - << "' not found" << messaget::eom; + cpp_typecheck.error() << "template scope '" << base_name << "' not found" + << messaget::eom; throw 0; } @@ -1024,8 +1023,8 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( { cpp_typecheck.show_instantiation_stack(cpp_typecheck.error()); cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "template scope `" << base_name - << "' is ambiguous" << messaget::eom; + cpp_typecheck.error() << "template scope '" << base_name << "' is ambiguous" + << messaget::eom; throw 0; } @@ -1197,7 +1196,7 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( if(instance.type.id()!=ID_struct) { cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() << "template `" + cpp_typecheck.error() << "template '" << base_name << "' is not a class" << messaget::eom; throw 0; } @@ -1243,9 +1242,8 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_namespace( if(id_set.empty()) { cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() - << "namespace `" - << base_name << "' not found" << messaget::eom; + cpp_typecheck.error() << "namespace '" << base_name << "' not found" + << messaget::eom; throw 0; } else if(id_set.size()==1) @@ -1256,9 +1254,8 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_namespace( else { cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() - << "namespace `" - << base_name << "' is ambiguous" << messaget::eom; + cpp_typecheck.error() << "namespace '" << base_name << "' is ambiguous" + << messaget::eom; throw 0; } } @@ -1444,22 +1441,18 @@ exprt cpp_typecheck_resolvet::resolve( if(qualified) { - cpp_typecheck.error() - << "symbol `" - << base_name << "' not found"; + cpp_typecheck.error() << "symbol '" << base_name << "' not found"; if(cpp_typecheck.cpp_scopes.current_scope().is_root_scope()) cpp_typecheck.error() << " in root scope"; else - cpp_typecheck.error() << " in scope `" - << cpp_typecheck.cpp_scopes.current_scope().prefix - << "'"; + cpp_typecheck.error() + << " in scope '" << cpp_typecheck.cpp_scopes.current_scope().prefix + << "'"; } else { - cpp_typecheck.error() - << "symbol `" - << base_name << "' is unknown"; + cpp_typecheck.error() << "symbol '" << base_name << "' is unknown"; } cpp_typecheck.error() << messaget::eom; @@ -1494,9 +1487,8 @@ exprt cpp_typecheck_resolvet::resolve( cpp_typecheck.show_instantiation_stack(cpp_typecheck.error()); cpp_typecheck.error().source_location=source_location; - cpp_typecheck.error() - << "template symbol `" - << base_name << "' is ambiguous" << messaget::eom; + cpp_typecheck.error() << "template symbol '" << base_name + << "' is ambiguous" << messaget::eom; throw 0; } @@ -1603,16 +1595,14 @@ exprt cpp_typecheck_resolvet::resolve( { cpp_typecheck.error().source_location=source_location; cpp_typecheck.error() - << "found no match for symbol `" << base_name - << "', candidates are:\n"; + << "found no match for symbol '" << base_name << "', candidates are:\n"; show_identifiers(base_name, identifiers, cpp_typecheck.error()); } else { cpp_typecheck.error().source_location=source_location; cpp_typecheck.error() - << "symbol `" << base_name - << "' does not uniquely resolve:\n"; + << "symbol '" << base_name << "' does not uniquely resolve:\n"; show_identifiers(base_name, new_identifiers, cpp_typecheck.error()); #ifdef DEBUG @@ -1660,7 +1650,7 @@ exprt cpp_typecheck_resolvet::resolve( cpp_typecheck.error().source_location=result.source_location()); cpp_typecheck.str - << "error: member `" << result.get(ID_component_name) + << "error: member '" << result.get(ID_component_name) << "' is not accessible"; throw 0; #endif @@ -1677,9 +1667,8 @@ exprt cpp_typecheck_resolvet::resolve( cpp_typecheck.error().source_location=source_location; cpp_typecheck.error() - << "error: expected expression, but got type `" - << cpp_typecheck.to_string(result.type()) << "'" - << messaget::eom; + << "error: expected expression, but got type '" + << cpp_typecheck.to_string(result.type()) << "'" << messaget::eom; throw 0; } @@ -1694,7 +1683,7 @@ exprt cpp_typecheck_resolvet::resolve( cpp_typecheck.error().source_location=source_location; cpp_typecheck.error() - << "error: expected type, but got expression `" + << "error: expected type, but got expression '" << cpp_typecheck.to_string(result) << "'" << messaget::eom; throw 0; diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 624be9badd9..c454a649920 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -95,7 +95,7 @@ void cpp_typecheckt::typecheck_class_template( if(previous.name!=symbol_name || id_set.size()>1) { error().source_location=cpp_name.source_location(); - str << "template declaration of `" << base_name.c_str() + str << "template declaration of '" << base_name.c_str() << " does not match previous declaration\n"; str << "location of previous definition: " << previous.location; throw 0; @@ -120,10 +120,9 @@ void cpp_typecheckt::typecheck_class_template( if(has_body && previous_has_body) { error().source_location=cpp_name.source_location(); - error() << "template struct `" << base_name - << "' defined previously\n" - << "location of previous definition: " - << previous_symbol.location << eom; + error() << "template struct '" << base_name << "' defined previously\n" + << "location of previous definition: " << previous_symbol.location + << eom; throw 0; } @@ -257,7 +256,7 @@ void cpp_typecheckt::typecheck_function_template( if(has_value && previous_has_value) { error().source_location=cpp_name.source_location(); - error() << "function template symbol `" << base_name + error() << "function template symbol '" << base_name << "' declared previously\n" << "location of previous definition: " << previous_symbol->second.location << eom; @@ -358,24 +357,24 @@ void cpp_typecheckt::typecheck_class_template_member( { error() << cpp_scopes.current_scope(); error().source_location=cpp_name.source_location(); - error() << "class template `" - << cpp_name.get_sub().front().get(ID_identifier) - << "' not found" << eom; + error() << "class template '" + << cpp_name.get_sub().front().get(ID_identifier) << "' not found" + << eom; throw 0; } else if(id_set.size()>1) { error().source_location=cpp_name.source_location(); - error() << "class template `" - << cpp_name.get_sub().front().get(ID_identifier) - << "' is ambiguous" << eom; + error() << "class template '" + << cpp_name.get_sub().front().get(ID_identifier) << "' is ambiguous" + << eom; throw 0; } else if((*(id_set.begin()))->id_class!=cpp_idt::id_classt::TEMPLATE) { // std::cerr << *(*id_set.begin()) << '\n'; error().source_location=cpp_name.source_location(); - error() << "class template `" + error() << "class template '" << cpp_name.get_sub().front().get(ID_identifier) << "' is not a template" << eom; throw 0; @@ -561,14 +560,13 @@ void cpp_typecheckt::convert_class_template_specialization( if(id_set.empty()) { error().source_location=type.source_location(); - error() << "class template `" << base_name << "' not found" << eom; + error() << "class template '" << base_name << "' not found" << eom; throw 0; } else if(id_set.size()>1) { error().source_location=type.source_location(); - error() << "class template `" << base_name << "' is ambiguous" - << eom; + error() << "class template '" << base_name << "' is ambiguous" << eom; throw 0; } @@ -661,15 +659,13 @@ void cpp_typecheckt::convert_template_function_or_member_specialization( if(id_set.empty()) { error().source_location=cpp_name.source_location(); - error() << "template function `" << base_name << "' not found" - << eom; + error() << "template function '" << base_name << "' not found" << eom; throw 0; } else if(id_set.size()>1) { error().source_location=cpp_name.source_location(); - error() << "template function `" << base_name - << "' is ambiguous" << eom; + error() << "template function '" << base_name << "' is ambiguous" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_using.cpp b/src/cpp/cpp_typecheck_using.cpp index 870bcd78254..6ca05826dce 100644 --- a/src/cpp/cpp_typecheck_using.cpp +++ b/src/cpp/cpp_typecheck_using.cpp @@ -36,10 +36,8 @@ void cpp_typecheckt::convert(cpp_usingt &cpp_using) if(id_set.empty()) { error().source_location=cpp_using.name().source_location(); - error() << "using " - << (using_directive?"namespace":"identifier") - << " `" - << base_name << "' not found" << eom; + error() << "using " << (using_directive ? "namespace" : "identifier") + << " '" << base_name << "' not found" << eom; throw 0; } diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 8c386779f12..b869257466d 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -499,7 +499,7 @@ bool Parser::SyntaxError() source_location.set_file(t[0].filename); source_location.set_line(std::to_string(t[0].line_no)); - std::string message="parse error before `"; + std::string message = "parse error before '"; for(std::size_t i=0; isource_location.set_comment(comment_t); @@ -667,7 +667,7 @@ void cover_mcdc_instrumentert::instrument( i_it->source_location.set_property_class(property_class); i_it->source_location.set_function(function_id); - std::string comment_f = description + " `" + p_string + "' false"; + std::string comment_f = description + " '" + p_string + "' false"; goto_program.insert_before_swap(i_it); *i_it = goto_programt::make_assertion(p, source_location); i_it->source_location.set_comment(comment_f); @@ -691,7 +691,7 @@ void cover_mcdc_instrumentert::instrument( std::string p_string = from_expr(ns, function_id, p); std::string description = - "MC/DC independence condition `" + p_string + "'"; + "MC/DC independence condition '" + p_string + "'"; goto_program.insert_before_swap(i_it); *i_it = goto_programt::make_assertion(not_exprt(p), source_location); diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index 973b607fa97..1387213353a 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -60,7 +60,7 @@ void cover_cover_instrumentert::instrument( code_function_call.arguments().size() == 1) { const exprt c = code_function_call.arguments()[0]; - std::string comment = "condition `" + from_expr(ns, function_id, c) + "'"; + std::string comment = "condition '" + from_expr(ns, function_id, c) + "'"; i_it->guard = not_exprt(c); i_it->type = ASSERT; i_it->code.clear(); diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 905ea89f3ad..60631e2a2eb 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -53,7 +53,7 @@ code_function_callt function_to_call( to_code_type(s_it->second.type).parameters().size()!=1 || to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer) { - std::string error="function `"+id2string(id)+"' has wrong signature"; + std::string error = "function '" + id2string(id) + "' has wrong signature"; throw error; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6cbd1cf9fef..6442032fc38 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -663,7 +663,7 @@ int goto_instrument_parse_optionst::doit() #endif if(!out) { - log.error() << "failed to write to `" << cmdline.args[1] << "'"; + log.error() << "failed to write to '" << cmdline.args[1] << "'"; return CPROVER_EXIT_CONVERSION_FAILED; } if(is_header) @@ -840,7 +840,7 @@ int goto_instrument_parse_optionst::doit() // write new binary? if(cmdline.args.size()==2) { - log.status() << "Writing GOTO program to `" << cmdline.args[1] << "'" + log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'" << messaget::eom; if(write_goto_binary(cmdline.args[1], goto_model, ui_message_handler)) @@ -927,7 +927,7 @@ void goto_instrument_parse_optionst::do_remove_returns() void goto_instrument_parse_optionst::get_goto_program() { - log.status() << "Reading GOTO program from `" << cmdline.args[0] << "'" + log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'" << messaget::eom; config.set(cmdline); @@ -1115,7 +1115,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); - log.status() << "Inlining calls of function `" << function << "'" + log.status() << "Inlining calls of function '" << function << "'" << messaget::eom; if(!cmdline.isset("log")) @@ -1342,7 +1342,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } else { - log.error() << "Unknown weak memory model `" << mm << "'" + log.error() << "Unknown weak memory model '" << mm << "'" << messaget::eom; model=Unknown; } diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index bc0c6efc728..facde1d01a8 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -164,16 +164,17 @@ get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler) } if(matches.empty()) - throw "interrupt handler `"+id2string(interrupt_handler)+"' not found"; + throw "interrupt handler '" + id2string(interrupt_handler) + "' not found"; if(matches.size()>=2) - throw "interrupt handler `"+id2string(interrupt_handler)+"' is ambiguous"; + throw "interrupt handler '" + id2string(interrupt_handler) + + "' is ambiguous"; symbol_exprt isr=matches.front(); if(!to_code_type(isr.type()).parameters().empty()) - throw "interrupt handler `"+id2string(interrupt_handler)+ - "' must not have parameters"; + throw "interrupt handler '" + id2string(interrupt_handler) + + "' must not have parameters"; return isr; } diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-instrument/undefined_functions.cpp index 99f1f72b6ed..55c1f9ee043 100644 --- a/src/goto-instrument/undefined_functions.cpp +++ b/src/goto-instrument/undefined_functions.cpp @@ -60,6 +60,6 @@ void undefined_function_abort_path(goto_modelt &goto_model) ins = goto_programt::make_assumption(false_exprt(), ins.source_location); ins.source_location.set_comment( - "`"+id2string(function)+"' is undefined"); + "'" + id2string(function) + "' is undefined"); } } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 025ac24f0ac..1f00aaa2a23 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -41,15 +41,14 @@ void goto_convertt::do_prob_uniform( if(arguments.size()!=2) { error().source_location=function.find_source_location(); - error() << "`" << identifier - << "' expected to have two arguments" << eom; + error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have LHS" << eom; + error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } @@ -60,7 +59,7 @@ void goto_convertt::do_prob_uniform( lhs.type().id()!=ID_signedbv) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected other type" << eom; + error() << "'" << identifier << "' expected other type" << eom; throw 0; } @@ -68,7 +67,7 @@ void goto_convertt::do_prob_uniform( arguments[1].type().id()!=lhs.type().id()) { error().source_location=function.find_source_location(); - error() << "`" << identifier + error() << "'" << identifier << "' expected operands to be of same type as LHS" << eom; throw 0; } @@ -77,7 +76,7 @@ void goto_convertt::do_prob_uniform( !arguments[1].is_constant()) { error().source_location=function.find_source_location(); - error() << "`" << identifier + error() << "'" << identifier << "' expected operands to be constant literals" << eom; throw 0; } @@ -120,15 +119,14 @@ void goto_convertt::do_prob_coin( if(arguments.size()!=2) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have two arguments" - << eom; + error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have LHS" << eom; + error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } @@ -137,7 +135,7 @@ void goto_convertt::do_prob_coin( if(lhs.type()!=bool_typet()) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected bool" << eom; + error() << "'" << identifier << "' expected bool" << eom; throw 0; } @@ -145,7 +143,7 @@ void goto_convertt::do_prob_coin( arguments[0].id()!=ID_constant) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected first operand to be " + error() << "'" << identifier << "' expected first operand to be " << "a constant literal of type unsigned long" << eom; throw 0; } @@ -155,7 +153,7 @@ void goto_convertt::do_prob_coin( arguments[1].id() != ID_constant) { error().source_location = function.find_source_location(); - error() << "`" << identifier << "' expected second operand to be " + error() << "'" << identifier << "' expected second operand to be " << "a constant literal of type unsigned long" << eom; throw 0; } @@ -630,15 +628,14 @@ void goto_convertt::do_function_call_symbol( if(ns.lookup(identifier, symbol)) { error().source_location=function.find_source_location(); - error() << "error: function `" << identifier << "' not found" - << eom; + error() << "error: function '" << identifier << "' not found" << eom; throw 0; } if(symbol->type.id()!=ID_code) { error().source_location=function.find_source_location(); - error() << "error: function `" << identifier + error() << "error: function '" << identifier << "' type mismatch: expected code" << eom; throw 0; } @@ -665,8 +662,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=1) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have one argument" - << eom; + error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -689,8 +685,7 @@ void goto_convertt::do_function_call_symbol( if(!arguments.empty()) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have no arguments" - << eom; + error() << "'" << identifier << "' expected to have no arguments" << eom; throw 0; } @@ -720,8 +715,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=1) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have one argument" - << eom; + error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -747,8 +741,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=2) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have two arguments" - << eom; + error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } @@ -789,8 +782,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=1) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have one argument" - << eom; + error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -944,7 +936,7 @@ void goto_convertt::do_function_call_symbol( arguments.size()!=3) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have four arguments" + error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; } @@ -985,7 +977,7 @@ void goto_convertt::do_function_call_symbol( else { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have four arguments" + error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; } @@ -1006,7 +998,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=4) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have four arguments" + error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; } @@ -1037,8 +1029,8 @@ void goto_convertt::do_function_call_symbol( if(arguments.empty()) { error().source_location=function.find_source_location(); - error() << "`" << identifier - << "' expected to have at least one argument" << eom; + error() << "'" << identifier << "' expected to have at least one argument" + << eom; throw 0; } @@ -1068,8 +1060,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=1) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have one argument" - << eom; + error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -1106,8 +1097,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=2) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have two arguments" - << eom; + error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } @@ -1131,8 +1121,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=2) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have two arguments" - << eom; + error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } @@ -1167,8 +1156,7 @@ void goto_convertt::do_function_call_symbol( if(arguments.size()!=1) { error().source_location=function.find_source_location(); - error() << "`" << identifier << "' expected to have one argument" - << eom; + error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -1207,9 +1195,8 @@ void goto_convertt::do_function_call_symbol( arguments[1].type()!=float_type())) { error().source_location=function.find_source_location(); - error() << "`" << identifier - << "' expected to have two float/double arguments" - << eom; + error() << "'" << identifier + << "' expected to have two float/double arguments" << eom; throw 0; } diff --git a/src/goto-programs/format_strings.cpp b/src/goto-programs/format_strings.cpp index 97a57780604..c16aff995b5 100644 --- a/src/goto-programs/format_strings.cpp +++ b/src/goto-programs/format_strings.cpp @@ -40,7 +40,7 @@ void parse_flags( curtok.flags.push_back(format_tokent::flag_typet::SIGN); break; default: throw unsupported_operation_exceptiont( - std::string("unsupported format specifier flag: `") + *it + "'"); + std::string("unsupported format specifier flag: '") + *it + "'"); } it++; } @@ -179,7 +179,7 @@ void parse_conversion_specifier( default: throw unsupported_operation_exceptiont( - std::string("unsupported format conversion specifier: `") + *it + "'"); + std::string("unsupported format conversion specifier: '") + *it + "'"); } it++; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index d14329e27d4..0105943308f 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -162,14 +162,14 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) if(not_prefix) { debug().source_location = i.source_location; - debug() << "encountered goto `" << goto_label + debug() << "encountered goto '" << goto_label << "' that enters one or more lexical blocks; " << "omitting constructors and destructors" << eom; } else { debug().source_location = i.source_location; - debug() << "adding goto-destructor code on jump to `" << goto_label + debug() << "adding goto-destructor code on jump to '" << goto_label << "'" << eom; node_indext end_destruct = intersection_result.common_ancestor; diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 8808d8d4869..8db877b87ab 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -65,7 +65,7 @@ void goto_inlinet::parameter_assignments( if(it1==arguments.end()) { warning().source_location=source_location; - warning() << "call to `" << function_name << "': " + warning() << "call to '" << function_name << "': " << "not enough arguments, " << "inserting non-deterministic value" << eom; @@ -356,7 +356,7 @@ void goto_inlinet::expand_function_call( // it's recursive. // Uh. Buh. Give up. warning().source_location=function.find_source_location(); - warning() << "recursion is ignored on call to `" << identifier << "'" + warning() << "recursion is ignored on call to '" << identifier << "'" << eom; if(force_full) @@ -371,7 +371,7 @@ void goto_inlinet::expand_function_call( if(f_it==goto_functions.function_map.end()) { warning().source_location=function.find_source_location(); - warning() << "missing function `" << identifier << "' is ignored" << eom; + warning() << "missing function '" << identifier << "' is ignored" << eom; if(force_full) target->turn_into_skip(); @@ -439,7 +439,7 @@ void goto_inlinet::expand_function_call( if(no_body_set.insert(identifier).second) // newly inserted { warning().source_location = function.find_source_location(); - warning() << "no body for function `" << identifier << "'" << eom; + warning() << "no body for function '" << identifier << "'" << eom; } } } diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 190133c1541..dc31bd3e675 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -43,7 +43,7 @@ static bool generate_entry_point_for_function( { throw invalid_command_line_argument_exceptiont{ // NOLINTNEXTLINE(whitespace/braces) - std::string{"couldn't find function with name `"} + + std::string{"couldn't find function with name '"} + id2string(entry_function_name) + "' in symbol table", "--function"}; } @@ -99,7 +99,7 @@ goto_modelt initialize_goto_model( if(!infile) { throw system_exceptiont( - "Failed to open input file `" + filename + '\''); + "Failed to open input file '" + filename + '\''); } language_filet &lf=language_files.add_file(filename); @@ -108,7 +108,7 @@ goto_modelt initialize_goto_model( if(lf.language==nullptr) { throw invalid_source_file_exceptiont( - "Failed to figure out type of file `" + filename + '\''); + "Failed to figure out type of file '" + filename + '\''); } languaget &language=*lf.language; @@ -140,7 +140,7 @@ goto_modelt initialize_goto_model( if(read_object_and_link(file, goto_model, message_handler)) { throw invalid_source_file_exceptiont( - "failed to read object or link in file `" + file + '\''); + "failed to read object or link in file '" + file + '\''); } } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index b51ad3537ad..c6030a22833 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -112,7 +112,7 @@ void interpretert::show_state() if(pc==function->second.body.instructions.end()) { - status() << "End of function `" << function->first << "'\n"; + status() << "End of function '" << function->first << "'\n"; } else function->second.body.output_instruction( diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 4884e27d571..515a21aad28 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -147,7 +147,7 @@ void lazy_goto_modelt::initialize( if(!infile) { throw system_exceptiont( - "failed to open input file `" + filename + '\''); + "failed to open input file '" + filename + '\''); } language_filet &lf=add_language_file(filename); @@ -156,7 +156,7 @@ void lazy_goto_modelt::initialize( if(lf.language==nullptr) { throw invalid_source_file_exceptiont( - "failed to figure out type of file `" + filename + '\''); + "failed to figure out type of file '" + filename + '\''); } languaget &language=*lf.language; diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 8bdf7929eeb..7a6015b26ca 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -208,8 +208,8 @@ bool read_bin_goto_object( else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F') { if(!filename.empty()) - message.error() << "Sorry, but I can't read ELF binary `" - << filename << "'" << messaget::eom; + message.error() << "Sorry, but I can't read ELF binary '" << filename + << "'" << messaget::eom; else message.error() << "Sorry, but I can't read ELF binaries" << messaget::eom; @@ -218,7 +218,7 @@ bool read_bin_goto_object( } else { - message.error() << "`" << filename << "' is not a goto-binary" + message.error() << "'" << filename << "' is not a goto-binary" << messaget::eom; return true; } diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 8128c8377f7..8d11516a4af 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -72,8 +72,7 @@ static bool read_goto_binary( if(!in) { - message.error() << "Failed to open `" << filename << "'" - << messaget::eom; + message.error() << "Failed to open '" << filename << "'" << messaget::eom; return true; } @@ -81,7 +80,7 @@ static bool read_goto_binary( in.read(hdr, 8); if(!in) { - message.error() << "Failed to read header from `" << filename << "'" + message.error() << "Failed to read header from '" << filename << "'" << messaget::eom; return true; } diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 374991da80a..af7ed6d147a 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -171,8 +171,7 @@ bool write_goto_binary( if(!out) { messaget message(message_handler); - message.error() << - "Failed to open `" << filename << "'"; + message.error() << "Failed to open '" << filename << "'"; return true; } diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 8cc62d897e0..107e61d7383 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -60,7 +60,7 @@ void symex_assignt::assign_rec( } else throw unsupported_operation_exceptiont( - "assign_rec: unexpected assignment to member of `" + type.id_string() + + "assign_rec: unexpected assignment to member of '" + type.id_string() + "'"); } else if(lhs.id()==ID_if) @@ -105,7 +105,7 @@ void symex_assignt::assign_rec( } else throw unsupported_operation_exceptiont( - "assignment to `" + lhs.id_string() + "' not handled"); + "assignment to '" + lhs.id_string() + "' not handled"); } /// Assignment from the rhs value to the lhs variable diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 55ee9b67759..e73ebe97860 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -66,7 +66,7 @@ void goto_symext::parameter_assignments( { log.warning() << state.source.pc->source_location.as_string() << ": " - "call to `" + "call to '" << id2string(function_identifier) << "': " "not enough arguments, inserting non-deterministic value" diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index ad9aa00929a..6115eed0b87 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -77,7 +77,7 @@ bool jsil_entry_point( if(matches.empty()) { messaget message(message_handler); - message.error() << "main symbol `" << config.main.value() << "' not found" + message.error() << "main symbol '" << config.main.value() << "' not found" << messaget::eom; return true; // give up } @@ -85,7 +85,7 @@ bool jsil_entry_point( if(matches.size()>=2) { messaget message(message_handler); - message.error() << "main symbol `" << config.main.value() + message.error() << "main symbol '" << config.main.value() << "' is ambiguous" << messaget::eom; return true; } @@ -102,7 +102,7 @@ bool jsil_entry_point( if(s_it==symbol_table.symbols.end()) { messaget message(message_handler); - message.error() << "main symbol `" << id2string(main_symbol) + message.error() << "main symbol '" << id2string(main_symbol) << "' not in symbol table" << messaget::eom; return true; // give up, no main } @@ -113,8 +113,8 @@ bool jsil_entry_point( if(symbol.value.is_nil()) { messaget message(message_handler); - message.error() << "main symbol `" << main_symbol - << "' has no body" << messaget::eom; + message.error() << "main symbol '" << main_symbol << "' has no body" + << messaget::eom; return false; // give up } diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 83216035bb0..e2b76b6387d 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -126,8 +126,8 @@ void jsil_typecheckt::typecheck_type(typet &type) if(symbol_table.add(new_symbol)) { - error() << "failed to add parameter symbol `" - << new_symbol.name << "' in the symbol table" << eom; + error() << "failed to add parameter symbol '" << new_symbol.name + << "' in the symbol table" << eom; throw 0; } } @@ -290,8 +290,7 @@ void jsil_typecheckt::typecheck_expr_proto_field(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -306,8 +305,7 @@ void jsil_typecheckt::typecheck_expr_proto_obj(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands"; + error() << "operator '" << expr.id() << "' expects two operands"; throw 0; } @@ -322,8 +320,7 @@ void jsil_typecheckt::typecheck_expr_delete(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -338,8 +335,7 @@ void jsil_typecheckt::typecheck_expr_index(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -358,8 +354,7 @@ void jsil_typecheckt::typecheck_expr_has_field(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -374,8 +369,7 @@ void jsil_typecheckt::typecheck_expr_field(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects single operand" << eom; + error() << "operator '" << expr.id() << "' expects single operand" << eom; throw 0; } @@ -389,8 +383,7 @@ void jsil_typecheckt::typecheck_expr_base(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects single operand" << eom; + error() << "operator '" << expr.id() << "' expects single operand" << eom; throw 0; } @@ -404,8 +397,7 @@ void jsil_typecheckt::typecheck_expr_ref(exprt &expr) if(expr.operands().size()!=3) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects three operands" << eom; + error() << "operator '" << expr.id() << "' expects three operands" << eom; throw 0; } @@ -422,7 +414,7 @@ void jsil_typecheckt::typecheck_expr_ref(exprt &expr) else { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() + error() << "operator '" << expr.id() << "' expects reference type in the third parameter. Got:" << operand3.pretty() << eom; throw 0; @@ -434,8 +426,7 @@ void jsil_typecheckt::typecheck_expr_concatenation(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -450,8 +441,7 @@ void jsil_typecheckt::typecheck_expr_subtype(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -466,8 +456,7 @@ void jsil_typecheckt::typecheck_expr_binary_boolean(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -482,8 +471,7 @@ void jsil_typecheckt::typecheck_expr_binary_arith(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -499,8 +487,7 @@ void jsil_typecheckt::typecheck_exp_binary_equal(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -514,8 +501,7 @@ void jsil_typecheckt::typecheck_expr_binary_compare(exprt &expr) if(expr.operands().size()!=2) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects two operands" << eom; + error() << "operator '" << expr.id() << "' expects two operands" << eom; throw 0; } @@ -530,8 +516,7 @@ void jsil_typecheckt::typecheck_expr_unary_boolean(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects one operand" << eom; + error() << "operator '" << expr.id() << "' expects one operand" << eom; throw 0; } @@ -545,8 +530,7 @@ void jsil_typecheckt::typecheck_expr_unary_string(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects one operand" << eom; + error() << "operator '" << expr.id() << "' expects one operand" << eom; throw 0; } @@ -560,8 +544,7 @@ void jsil_typecheckt::typecheck_expr_unary_num(exprt &expr) if(expr.operands().size()!=1) { error().source_location = expr.source_location(); - error() << "operator `" << expr.id() - << "' expects one operand" << eom; + error() << "operator '" << expr.id() << "' expects one operand" << eom; throw 0; } @@ -627,9 +610,8 @@ void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr) if(symbol_table.add(new_symbol)) { - error() << "failed to add symbol `" - << new_symbol.name << "' in the symbol table" - << eom; + error() << "failed to add symbol '" << new_symbol.name + << "' in the symbol table" << eom; throw 0; } } diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index eab51721745..e85ccd1aab0 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -89,7 +89,7 @@ get_language_from_identifier(const namespacet &ns, const irep_idt &identifier) std::unique_ptr language = get_language_from_mode(mode); INVARIANT( language, - "symbol `" + id2string(identifier) + "' has unknown mode '" + + "symbol '" + id2string(identifier) + "' has unknown mode '" + id2string(mode) + "'"); return language; } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 18b25d069c9..a622fd6167e 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -379,13 +379,12 @@ void linkingt::link_error( { error().source_location=new_symbol.location; - error() << "error: " << msg << " `" - << old_symbol.display_name() - << "'" << '\n'; - error() << "old definition in module `" << old_symbol.module << "' " + error() << "error: " << msg << " '" << old_symbol.display_name() << "'" + << '\n'; + error() << "old definition in module '" << old_symbol.module << "' " << old_symbol.location << '\n' << type_to_string_verbose(old_symbol) << '\n'; - error() << "new definition in module `" << new_symbol.module << "' " + error() << "new definition in module '" << new_symbol.module << "' " << new_symbol.location << '\n' << type_to_string_verbose(new_symbol) << eom; } @@ -774,9 +773,10 @@ void linkingt::duplicate_code_symbol( // keep the one in old_symbol -- libraries come last! warning().source_location=new_symbol.location; - warning() << "function `" << old_symbol.name << "' in module `" - << new_symbol.module << "' is shadowed by a definition in module `" - << old_symbol.module << "'" << eom; + warning() << "function '" << old_symbol.name << "' in module '" + << new_symbol.module + << "' is shadowed by a definition in module '" + << old_symbol.module << "'" << eom; } else link_error( diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp index c0b843694ca..ff65e633ccc 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.cpp +++ b/src/memory-analyzer/memory_analyzer_parse_options.cpp @@ -105,7 +105,7 @@ int memory_analyzer_parse_optionst::doit() if(!opt.has_value()) { throw deserialization_exceptiont( - "cannot read goto binary `" + binary + "'"); + "cannot read goto binary '" + binary + "'"); } const goto_modelt goto_model(std::move(opt.value())); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index bc583e8e29e..d4db2a93d07 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1470,7 +1470,7 @@ void value_sett::assign_rec( // which we don't track } else - throw "assign NYI: `"+lhs.id_string()+"'"; + throw "assign NYI: '" + lhs.id_string() + "'"; } void value_sett::do_function_call( diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 5a991ee8b71..11d5abee6ac 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1258,7 +1258,7 @@ void value_set_fit::assign_rec( assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set); } else - throw "assign NYI: `"+lhs.id_string()+"'"; + throw "assign NYI: '" + lhs.id_string() + "'"; } void value_set_fit::do_function_call( diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 36839c3f601..40628640ec5 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1376,7 +1376,7 @@ void value_set_fivrt::assign_rec( assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set, true); } else - throw "assign NYI: `"+lhs.id_string()+"'"; + throw "assign NYI: '" + lhs.id_string() + "'"; } void value_set_fivrt::do_function_call( diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 4d9494458de..9acffd86c16 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -1037,7 +1037,7 @@ void value_set_fivrnst::assign_rec( assign_rec(lhs.op0(), values_rhs, suffix, ns, true); } else - throw "assign NYI: `"+lhs.id_string()+"'"; + throw "assign NYI: '" + lhs.id_string() + "'"; } void value_set_fivrnst::do_function_call( diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 71e80ccd4c3..c7592613e28 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -189,7 +189,7 @@ void arrayst::collect_arrays(const exprt &a) DATA_INVARIANT( to_member_expr(a).struct_op().id() == ID_symbol || to_member_expr(a).struct_op().id() == ID_nondet_symbol, - ("unexpected array expression: member with `" + a.op0().id_string() + "'") + ("unexpected array expression: member with '" + a.op0().id_string() + "'") .c_str()); } else if(a.id()==ID_constant || @@ -235,8 +235,8 @@ void arrayst::collect_arrays(const exprt &a) { DATA_INVARIANT( false, - ("unexpected array expression (collect_arrays): `"+ - a.id_string()+"'").c_str()); + ("unexpected array expression (collect_arrays): '" + a.id_string() + "'") + .c_str()); } } @@ -524,8 +524,9 @@ void arrayst::add_array_constraints( { DATA_INVARIANT( false, - ("unexpected array expression (add_array_constraints): `"+ - expr.id_string()+"'").c_str()); + ("unexpected array expression (add_array_constraints): '" + + expr.id_string() + "'") + .c_str()); } } diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index 4b3cdc647c5..3b855b05a92 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -203,7 +203,7 @@ void boolbvt::convert_with_struct( { DATA_INVARIANT_WITH_DIAGNOSTICS( subtype == op2.type(), - "with/struct: component `" + id2string(component_name) + + "with/struct: component '" + id2string(component_name) + "' type does not match", irep_pretty_diagnosticst{subtype}, irep_pretty_diagnosticst{op2.type()}); diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 0a9d3406c15..dc206b0db83 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -268,7 +268,7 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) { INVARIANT( !op.empty(), - "operator `" + expr.id_string() + "' takes at least one operand"); + "operator '" + expr.id_string() + "' takes at least one operand"); bvt bv; diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index eae03360156..ddd321356f5 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -353,7 +353,7 @@ void bv_refinementt::check_SAT(approximationt &a) UNREACHABLE; } - log.status() << "Found spurious `" << a.as_string() << "' (state " + log.status() << "Found spurious '" << a.as_string() << "' (state " << a.over_state << ")" << messaget::eom; progress=true; @@ -369,7 +369,7 @@ void bv_refinementt::check_UNSAT(approximationt &a) if(!this->conflicts_with(a)) return; - log.status() << "Found assumption for `" << a.as_string() + log.status() << "Found assumption for '" << a.as_string() << "' in proof (state " << a.under_state << ")" << messaget::eom; PRECONDITION(!a.under_assumptions.empty()); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 1868627547a..96e0e998a1a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1866,7 +1866,7 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_constraint_select_one) { UNEXPECTEDCASE( - "smt2_convt::convert_expr: `"+expr.id_string()+ + "smt2_convt::convert_expr: '" + expr.id_string() + "' is not yet supported"); } else if(expr.id() == ID_bswap) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 3db2057bd4f..ad422f5b8ea 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -354,8 +354,8 @@ exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op) if(op[i].type() != op[0].type()) { throw error() << "expression must have operands with matching types," - " but got `" - << smt2_format(op[0].type()) << "' and `" + " but got '" + << smt2_format(op[0].type()) << "' and '" << smt2_format(op[i].type()) << '\''; } } @@ -373,8 +373,8 @@ exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op) if(op[0].type() != op[1].type()) { throw error() << "expression must have operands with matching types," - " but got `" - << smt2_format(op[0].type()) << "' and `" + " but got '" + << smt2_format(op[0].type()) << "' and '" << smt2_format(op[1].type()) << '\''; } @@ -829,7 +829,7 @@ exprt smt2_parsert::function_application() return symbol_exprt(final_id, id_it->second.type); } - throw error() << "unknown function symbol `" << id << '\''; + throw error() << "unknown function symbol '" << id << '\''; } } break; @@ -935,7 +935,7 @@ exprt smt2_parsert::function_application() } else { - throw error() << "unknown indexed identifier `" + throw error() << "unknown indexed identifier '" << smt2_tokenizer.get_buffer() << '\''; } } @@ -1038,7 +1038,7 @@ exprt smt2_parsert::expression() return std::move(symbol_expr); } - throw error() << "unknown expression `" << identifier << '\''; + throw error() << "unknown expression '" << identifier << '\''; } } @@ -1100,7 +1100,7 @@ typet smt2_parsert::sort() else if(buffer=="Real") return real_typet(); else - throw error() << "unexpected sort: `" << buffer << '\''; + throw error() << "unexpected sort: '" << buffer << '\''; } case smt2_tokenizert::OPEN: @@ -1145,7 +1145,7 @@ typet smt2_parsert::sort() return ieee_float_spect(width_f - 1, width_e).to_type(); } else - throw error() << "unexpected sort: `" << smt2_tokenizer.get_buffer() + throw error() << "unexpected sort: '" << smt2_tokenizer.get_buffer() << '\''; } else if(smt2_tokenizer.get_buffer() == "Array") @@ -1166,7 +1166,7 @@ typet smt2_parsert::sort() throw error("unsupported array sort"); } else - throw error() << "unexpected sort: `" << smt2_tokenizer.get_buffer() + throw error() << "unexpected sort: '" << smt2_tokenizer.get_buffer() << '\''; case smt2_tokenizert::CLOSE: @@ -1175,7 +1175,7 @@ typet smt2_parsert::sort() case smt2_tokenizert::END_OF_FILE: case smt2_tokenizert::NONE: case smt2_tokenizert::KEYWORD: - throw error() << "unexpected token in a sort: `" + throw error() << "unexpected token in a sort: '" << smt2_tokenizer.get_buffer() << '\''; } @@ -1264,13 +1264,13 @@ void smt2_parsert::command(const std::string &c) // declare-var appears to be a synonym for declare-const that is // accepted by Z3 and CVC4 if(next_token() != smt2_tokenizert::SYMBOL) - throw error() << "expected a symbol after `" << c << '\''; + throw error() << "expected a symbol after '" << c << '\''; irep_idt id = smt2_tokenizer.get_buffer(); auto type = sort(); if(add_fresh_id(id, exprt(ID_nil, type)) != id) - throw error() << "identifier `" << id << "' defined twice"; + throw error() << "identifier '" << id << "' defined twice"; } else if(c=="declare-fun") { @@ -1281,7 +1281,7 @@ void smt2_parsert::command(const std::string &c) auto type = function_signature_declaration(); if(add_fresh_id(id, exprt(ID_nil, type)) != id) - throw error() << "identifier `" << id << "' defined twice"; + throw error() << "identifier '" << id << "' defined twice"; } else if(c == "define-const") { @@ -1296,14 +1296,14 @@ void smt2_parsert::command(const std::string &c) // check type of value if(value.type() != type) { - throw error() << "type mismatch in constant definition: expected `" - << smt2_format(type) << "' but got `" + throw error() << "type mismatch in constant definition: expected '" + << smt2_format(type) << "' but got '" << smt2_format(value.type()) << '\''; } // create the entry if(add_fresh_id(id, value) != id) - throw error() << "identifier `" << id << "' defined twice"; + throw error() << "identifier '" << id << "' defined twice"; } else if(c=="define-fun") { @@ -1327,21 +1327,21 @@ void smt2_parsert::command(const std::string &c) const auto &f_signature = to_mathematical_function_type(signature.type); if(body.type() != f_signature.codomain()) { - throw error() << "type mismatch in function definition: expected `" - << smt2_format(f_signature.codomain()) << "' but got `" + throw error() << "type mismatch in function definition: expected '" + << smt2_format(f_signature.codomain()) << "' but got '" << smt2_format(body.type()) << '\''; } } else if(body.type() != signature.type) { - throw error() << "type mismatch in function definition: expected `" - << smt2_format(signature.type) << "' but got `" + throw error() << "type mismatch in function definition: expected '" + << smt2_format(signature.type) << "' but got '" << smt2_format(body.type()) << '\''; } // create the entry if(add_fresh_id(id, body) != id) - throw error() << "identifier `" << id << "' defined twice"; + throw error() << "identifier '" << id << "' defined twice"; id_map.at(id).type = signature.type; id_map.at(id).parameters = signature.parameters; diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index ba2cd9db4a9..759913461d5 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -195,12 +195,12 @@ void smt2_solvert::command(const std::string &c) const auto id_map_it = id_map.find(identifier); if(id_map_it == id_map.end()) - throw error() << "unexpected symbol `" << identifier << '\''; + throw error() << "unexpected symbol '" << identifier << '\''; const exprt value = solver.get(op); if(value.is_nil()) - throw error() << "no value for `" << identifier << '\''; + throw error() << "no value for '" << identifier << '\''; values.push_back(value); } diff --git a/src/solvers/smt2/smt2_tokenizer.cpp b/src/solvers/smt2/smt2_tokenizer.cpp index 994c3e7699c..a6395a56fad 100644 --- a/src/solvers/smt2/smt2_tokenizer.cpp +++ b/src/solvers/smt2/smt2_tokenizer.cpp @@ -305,7 +305,7 @@ void smt2_tokenizert::get_token_from_stream() else { // illegal character, error - throw error() << "unexpected character `" << ch << '\''; + throw error() << "unexpected character '" << ch << '\''; } } } diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index da3de863218..9f42956a915 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -45,7 +45,7 @@ static void run_symtab2gb( std::ofstream out_file{gb_filename, std::ios::binary}; if(!out_file.is_open()) { - throw system_exceptiont{"couldn't open output file `" + gb_filename + "'"}; + throw system_exceptiont{"couldn't open output file '" + gb_filename + "'"}; } std::vector symtab_files; for(auto const &symtab_filename : symtab_filenames) @@ -53,7 +53,7 @@ static void run_symtab2gb( std::ifstream symtab_file{symtab_filename}; if(!symtab_file.is_open()) { - throw system_exceptiont{"couldn't open input file `" + symtab_filename + + throw system_exceptiont{"couldn't open input file '" + symtab_filename + "'"}; } symtab_files.emplace_back(std::move(symtab_file)); @@ -73,13 +73,13 @@ static void run_symtab2gb( if(failed(symtab_language->parse(symtab_file, symtab_filename))) { throw invalid_source_file_exceptiont{ - "failed to parse symbol table from file `" + symtab_filename + "'"}; + "failed to parse symbol table from file '" + symtab_filename + "'"}; } symbol_tablet symtab{}; if(failed(symtab_language->typecheck(symtab, ""))) { throw invalid_source_file_exceptiont{ - "failed to typecheck symbol table from file `" + symtab_filename + "'"}; + "failed to typecheck symbol table from file '" + symtab_filename + "'"}; } goto_modelt goto_model{}; goto_model.symbol_table = symtab; diff --git a/src/util/array_name.cpp b/src/util/array_name.cpp index 731a41a84d9..bcf3cd11405 100644 --- a/src/util/array_name.cpp +++ b/src/util/array_name.cpp @@ -29,12 +29,12 @@ std::string array_name( { const symbolt &symbol= ns.lookup(to_ssa_expr(expr).get_object_name()); - return "array `"+id2string(symbol.base_name)+"'"; + return "array '" + id2string(symbol.base_name) + "'"; } else if(expr.id()==ID_symbol) { const symbolt &symbol = ns.lookup(to_symbol_expr(expr)); - return "array `"+id2string(symbol.base_name)+"'"; + return "array '" + id2string(symbol.base_name) + "'"; } else if(expr.id()==ID_string_constant) { diff --git a/src/util/config.cpp b/src/util/config.cpp index a943ceb74c2..cac312f4a97 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1140,7 +1140,7 @@ static irep_idt string_from_ns( to_address_of_expr(tmp).object().id() == ID_index && to_index_expr(to_address_of_expr(tmp).object()).array().id() == ID_string_constant, - "symbol table configuration entry `" + id2string(id) + + "symbol table configuration entry '" + id2string(id) + "' must be a string constant"); return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value); @@ -1161,7 +1161,7 @@ static unsigned unsigned_from_ns( INVARIANT( tmp.id() == ID_constant, - "symbol table configuration entry `" + id2string(id) + + "symbol table configuration entry '" + id2string(id) + "' must be a constant"); mp_integer int_value; @@ -1169,7 +1169,7 @@ static unsigned unsigned_from_ns( const bool error = to_integer(to_constant_expr(tmp), int_value); INVARIANT( !error, - "symbol table configuration entry `" + id2string(id) + + "symbol table configuration entry '" + id2string(id) + "' must be convertible to mp_integer"); return numeric_cast_v(int_value); diff --git a/src/util/get_module.cpp b/src/util/get_module.cpp index 376cab2adc3..f3df545efeb 100644 --- a/src/util/get_module.cpp +++ b/src/util/get_module.cpp @@ -53,12 +53,12 @@ const symbolt &get_module_by_name( if(symbolptr_list.empty()) { - message.error() << "module `" << module << "' not found" << messaget::eom; + message.error() << "module '" << module << "' not found" << messaget::eom; throw 0; } else if(symbolptr_list.size()>=2) { - message.error() << "module `" << module << "' does not uniquely resolve:\n"; + message.error() << "module '" << module << "' does not uniquely resolve:\n"; forall_symbolptr_list(it, symbolptr_list) message.error() << " " << (*it)->name << '\n'; @@ -123,7 +123,7 @@ const symbolt &get_module( const symbolt &symbol=*symbolptr_list.front(); - message.status() << "Using module `" << symbol.pretty_name << "'" + message.status() << "Using module '" << symbol.pretty_name << "'" << messaget::eom; return symbol; diff --git a/src/util/parser.cpp b/src/util/parser.cpp index b2a846e932a..efe5f0bba73 100644 --- a/src/util/parser.cpp +++ b/src/util/parser.cpp @@ -33,14 +33,14 @@ void parsert::parse_error( { std::string tmp=message; if(!before.empty()) - tmp+=" before `"+before+"'"; + tmp += " before '" + before + "'"; - #if 0 +#if 0 source_locationt tmp_source_location=source_location; tmp_source_location.set_column(column-before.size()); print(1, tmp, -1, tmp_source_location); - #else +#else error().source_location=source_location; error() << tmp << eom; - #endif +#endif } diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index a081a9cc949..68333a414a6 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -112,7 +112,7 @@ void split_string( split_string(s, delim, result, strip); if(result.size() != 2) { - throw deserialization_exceptiont{"expected string `" + s + + throw deserialization_exceptiont{"expected string '" + s + "' to contain two substrings " "delimited by " + delim + " but has " + From f0c015193a9336f9c140340fb81267a5b7e854a5 Mon Sep 17 00:00:00 2001 From: Owen Date: Mon, 8 Jul 2019 11:55:37 +0100 Subject: [PATCH 2/3] Remove erroneous backtick --- src/cpp/cpp_typecheck_compound_type.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index c4309c77629..056a91d83f0 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -374,7 +374,7 @@ void cpp_typecheckt::typecheck_compound_declarator( if(is_cast_operator && is_static) { error().source_location=cpp_name.source_location(); - error() << "cast operators cannot be static`" << eom; + error() << "cast operators cannot be static" << eom; throw 0; } From 4c900d1bf8dda708f9b63812114faecf366490f5 Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 9 Jul 2019 09:44:52 +0100 Subject: [PATCH 3/3] Do not quote classes we fail to load The error message used to be failed to load class 'Test' This commit makes it failed to load class Test The reasoning is that there is no need to quote the class name, it is totally clear where it starts and where it ends. --- jbmc/regression/jbmc/classpath-invalid/test-jar.desc | 2 +- jbmc/regression/jbmc/classpath-invalid/test-path.desc | 2 +- jbmc/regression/jbmc/generics_type_param/test.desc | 6 +++--- jbmc/src/java_bytecode/java_class_loader.cpp | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/jbmc/regression/jbmc/classpath-invalid/test-jar.desc b/jbmc/regression/jbmc/classpath-invalid/test-jar.desc index f0545562fa7..9dd9c6081fb 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test-jar.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test-jar.desc @@ -4,7 +4,7 @@ Test.class ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ -^failed to load class 'Test'$ +^failed to load class Test$ -- -- symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/jbmc/regression/jbmc/classpath-invalid/test-path.desc b/jbmc/regression/jbmc/classpath-invalid/test-path.desc index f3b70faa9d3..354e216bfc4 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test-path.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test-path.desc @@ -4,7 +4,7 @@ Test.class ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ -^failed to load class 'Test'$ +^failed to load class Test$ -- -- symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/jbmc/regression/jbmc/generics_type_param/test.desc b/jbmc/regression/jbmc/generics_type_param/test.desc index 9e1b87c986a..3ff92f6b66f 100644 --- a/jbmc/regression/jbmc/generics_type_param/test.desc +++ b/jbmc/regression/jbmc/generics_type_param/test.desc @@ -7,6 +7,6 @@ Reading class AWrapper Reading class FWrapper Reading class IWrapper -- -failed to load class \'AWrapper\' -failed to load class \'FWrapper\' -failed to load class \'IWrapper\' +failed to load class AWrapper +failed to load class FWrapper +failed to load class IWrapper diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 9034345a54a..3750d11f1ca 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -176,7 +176,7 @@ java_class_loadert::get_parse_tree( return parse_trees; // Not found or failed to load - warning() << "failed to load class \'" << class_name << '\'' << eom; + warning() << "failed to load class " << class_name << eom; parse_trees.emplace_back(class_name); return parse_trees; }