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..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 282ae0209f8..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/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..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/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..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; } @@ -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..056a91d83f0 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; } } @@ -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; } @@ -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 " +