diff --git a/regression/cbmc/xml-escaping/debug_output.desc b/regression/cbmc/xml-escaping/debug_output.desc new file mode 100644 index 00000000000..ddfb415c818 --- /dev/null +++ b/regression/cbmc/xml-escaping/debug_output.desc @@ -0,0 +1,13 @@ +CORE +main.c +--verbosity 10 --xml-ui +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +⇔ false +\¬main\:\:1\:\:x\!0\@1\#1 +-- +XML does not support escaping non-printable character +-- +Test that running cbmc with --verbosity 10 and --xml-ui does not violate any +xml printing invariants. diff --git a/regression/cbmc/xml-escaping/main.c b/regression/cbmc/xml-escaping/main.c new file mode 100644 index 00000000000..f25cc971824 --- /dev/null +++ b/regression/cbmc/xml-escaping/main.c @@ -0,0 +1,8 @@ +#include + +int main(void) +{ + __CPROVER_bool x; + __CPROVER_assume(!x); + assert(0); +} diff --git a/src/util/xml.cpp b/src/util/xml.cpp index 7a16e4e6ed3..803037b68a1 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -108,7 +108,7 @@ void xmlt::escape(const std::string &s, std::ostream &out) default: DATA_INVARIANT( - ch >= ' ', + static_cast(ch) >= 32u, "XML does not support escaping non-printable character " + std::to_string((unsigned char)ch)); out << ch; @@ -149,7 +149,7 @@ void xmlt::escape_attribute(const std::string &s, std::ostream &out) default: DATA_INVARIANT( - ch >= ' ', + static_cast(ch) >= 32u, "XML does not support escaping non-printable character " + std::to_string((unsigned char)ch)); out << ch;