CBMC dumps core on simple example #5293
Description
test.c is:
#include <assert.h>
void* nondet_voidp();
int main()
{
void* p;
*p;
}
CBMC version: CBMC version 5.12 (cbmc-5.12-156-g8911c0adb) 64-bit x86_64 macos
Operating system: OSX
Exact command line resulting in the issue: cbmc --bounds-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwind 1 --unwinding-assertions test.c
What behaviour did you expect: CBMC not to crash
What happened instead: CBMC crashed
CBMC version 5.12 (cbmc-5.12-156-g8911c0adb) 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
--- begin invariant violation report ---
Invariant check failed
File: ../src/analyses/goto_check.cpp:1150 function: pointer_validity_check
Condition: size_of_expr_opt.has_value()
Reason: Check return value
Backtrace:
0 cbmc 0x000000010e413d81 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 81
1 cbmc 0x000000010e4143e3 _Z13get_backtracev + 67
2 cbmc 0x000000010d1edd91 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 49
3 cbmc 0x000000010d1edd23 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 51
4 cbmc 0x000000010d8b7d4d _ZN11goto_checkt22pointer_validity_checkERK17dereference_exprtRK5exprtRK11guard_exprt + 253
5 cbmc 0x000000010d8be9bb _ZN11goto_checkt9check_recERK5exprtR11guard_exprt + 1659
6 cbmc 0x000000010d8be5b0 _ZN11goto_checkt9check_recERK5exprtR11guard_exprt + 624
7 cbmc 0x000000010d8c00a4 _ZN11goto_checkt5checkERK5exprt + 100
8 cbmc 0x000000010d8c176e _ZN11goto_checkt10goto_checkERK8dstringtR14goto_functiont + 3710
9 cbmc 0x000000010d8c5717 _Z10goto_checkRK10namespacetRK8optionstR15goto_functionst + 247
10 cbmc 0x000000010d8c58d5 _Z10goto_checkRK8optionstR11goto_modelt + 69
11 cbmc 0x000000010d212101 _ZN19cbmc_parse_optionst20process_goto_programER11goto_modeltRK8optionstR8messaget + 929
12 cbmc 0x000000010d2107ae _ZN19cbmc_parse_optionst16get_goto_programER11goto_modeltRK8optionstRK8cmdlinetR19ui_message_handlert + 414
13 cbmc 0x000000010d20e868 _ZN19cbmc_parse_optionst4doitEv + 2856
14 cbmc 0x000000010e491785 _ZN19parse_options_baset4mainEv + 1781
15 cbmc 0x000000010d1ece32 main + 66
16 libdyld.dylib 0x00007fff59ab23d5 start + 1
17 ??? 0x000000000000000e 0x0 + 14
--- end invariant violation report ---
Abort trap: 6