Description
This test is the same one in #7185, but with an extra assert:
#include <assert.h>
struct Unit
{
};
int main() {
struct Unit var_0;
int x;
int y = x;
assert(0);
assert(y == x);
return 0;
}Running it with --z3 and --json-ui causes an invariant violation:
$ cbmc unit2.c --z3 --json-ui
[
{
"program": "CBMC 5.69.1 (cbmc-5.69.1)"
},
{
"messageText": "CBMC version 5.69.1 (cbmc-5.69.1) 64-bit x86_64 linux",
"messageType": "STATUS-MESSAGE"
},
{
"messageText": "Parsing unit2.c",
"messageType": "STATUS-MESSAGE"
# -- snip --
}--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:121 function: convert_decl
Condition: step.full_lhs_value.is_not_nil()
Reason: full_lhs_value in assignment must not be nil
Backtrace:
cbmc(+0xa8bde0) [0x559203cd5de0]
cbmc(+0xa8c389) [0x559203cd6389]
cbmc(+0x1e7d98) [0x559203431d98]
cbmc(+0x6853c6) [0x5592038cf3c6]
cbmc(+0x33d9f2) [0x5592035879f2]
cbmc(+0x357cac) [0x5592035a1cac]
cbmc(+0x1ef124) [0x559203439124]
cbmc(+0x1ee5fa) [0x5592034385fa]
cbmc(+0x1e5e2f) [0x55920342fe2f]
cbmc(+0x1d1e39) [0x55920341be39]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f8da07cc0b3]
cbmc(+0x1e77ae) [0x5592034317ae]
--- end invariant violation report ---
Aborted (core dumped)
This doesn't crash if I remove either of the --z3 or the --json-ui options.
CBMC version: 5.69.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc unit2.c --z3 --json-ui
What behaviour did you expect: Verification fails
What happened instead: CBMC crashed