-
Notifications
You must be signed in to change notification settings - Fork 283
Open
Labels
ViewerBugs and features related to CBMC ViewerBugs and features related to CBMC ViewerawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC userspending merge
Description
CBMC version: 5.53.1
Operating system: linux
Exact command line resulting in the issue: cbmc issue.c --trace --xml-ui
What behaviour did you expect: Successfully generated xml file
What happened instead: Program aborted with an error
Problem program issue.c:
#include <stdlib.h>
int main(void) {
const unsigned char *str = (unsigned char *)"\x00";
assert(*str == "\x01");
return 0;
}
Last several lines of output when running cbmc issue.c --trace --xml-ui:
--- begin invariant violation report ---
Invariant check failed
File: xml.cpp:154 function: escape_attribute
Condition: ch >= ' '
Reason: XML does not support escaping non-printable character 1
Backtrace:
cbmc() [0x6561cd]
cbmc() [0x6571b7]
cbmc() [0x56a612]
cbmc() [0x6e4f49]
cbmc() [0x6e5052]
cbmc() [0x6e50dd]
cbmc() [0x6e50dd]
cbmc() [0xcf28ed]
cbmc() [0x918641]
cbmc() [0x700058]
cbmc() [0x6ff52a]
cbmc() [0x55ddeb]
cbmc() [0x551e01]
/lib64/libc.so.6(__libc_start_main+0xea) [0x7f8ed496a13a]
cbmc() [0x55ea2a]
--- end invariant violation report ---
[1] 1659 abort cbmc expr.c --trace --xml-ui
Metadata
Metadata
Assignees
Labels
ViewerBugs and features related to CBMC ViewerBugs and features related to CBMC ViewerawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC userspending merge