cbmc --show-properties fails #8165
Description
CBMC version: CBMC version 6.0.0-preview (9d28845) 64-bit x86_64 linux
Operating system: ubuntu (on github worker)
Exact command line resulting in the issue: cbmc --show-properties xen_4_13/xen/xen-syms
What behaviour did you expect: CBMC should show the properties in the binary, instead of crashing with an assertion
What happened instead: CBMC crashed
I created a reproducer as part of the CBMC workflow. Once fixed, that change could be added to the github workflows of CBMC: nmanthey#6
Full trace:
cbmc --show-properties xen_4_13/xen/xen-syms
$(pwd)/src/cbmc/cbmc --show-properties xen_4_13/xen/xen-syms
shell: /usr/bin/bash -e {0}
env:
CCACHE_BASEDIR: /home/runner/work/cbmc/cbmc
CCACHE_DIR: /home/runner/work/cbmc/cbmc/.ccache
CBMC version 6.0.0-preview (9d28845a) 64-bit x86_64 linux
Reading GOTO program from file xen_4_13/xen/xen-syms
Generating GOTO Program
--- begin invariant violation report ---
Invariant check failed
File: remove_asm.cpp:138 function: gcc_asm_function_call
Condition: symbol_table.lookup_ref(function_identifier).type == fkt_type
Reason: function types should match
Backtrace:
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x4f10aa]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x4f1710]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x42217d]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x41b286]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x90c405]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x90e2c5]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x910a23]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x910b90]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x5aaa3c]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x5aa7ba]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x5a8baa]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0xafb5c3]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x5a42c2]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7fe9faff0083]
/home/runner/work/cbmc/cbmc/src/cbmc/cbmc() [0x40ac7e]
--- end invariant violation report ---