Merge pull request #7109 from thomasspriggs/tas/xml_invariant

Allow characters with value >= 128 in XML output

Author: thomasspriggs

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.

regression/cbmc/xml-escaping/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main(void)
+{
+  __CPROVER_bool x;
+  __CPROVER_assume(!x);
+  assert(0);
+}

src/util/xml.cpp

@@ -108,7 +108,7 @@ void xmlt::escape(const std::string &s, std::ostream &out)
 
     default:
       DATA_INVARIANT(
-        ch >= ' ',
+        static_cast<unsigned char>(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<unsigned char>(ch) >= 32u,
         "XML does not support escaping non-printable character " +
           std::to_string((unsigned char)ch));
       out << ch;