Memory blowup during typechecking

[remi-delmas-3000]

This is a macro checks that its argument is a literal constant by placing it an type expression where only literal constants are expected. Clang typechecks the model in a few milliseconds.

#define CHECK_CONSTANT(x) sizeof((struct { char c[x]; }){{0}}.c)
int main() {
  CHECK_CONSTANT(0xFFFFFFFFU);
  return 0;
}

cbmc hangs during typechecking, memory blows up and it crashes with an invariant violation after a while,

--- begin invariant violation report ---
Invariant check failed
File: /Users/delmasrd/projects/cbmc/src/util/irep.h:562 function: remove_ref
Condition: old_data->ref_count != 0
Reason: Precondition
Backtrace:
0   cbmc                                0x00000001018ad65a _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x00000001018adbd8 _Z13get_backtracev + 184
2   cbmc                                0x0000000101237d3c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   cbmc                                0x0000000101237c89 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   cbmc                                0x0000000101237be8 _ZN13sharing_treetI5irept20forward_list_as_maptI8dstringtS0_EE10remove_refEP10tree_nodetIS0_S3_Lb1EE + 248
5   cbmc                                0x0000000101470156 _ZN17c_typecheck_baset25do_designated_initializerER5exprtR11designatortRKS0_NSt3__111__wrap_iterIPS4_EEb + 1382
6   cbmc                                0x0000000101473e11 _ZN17c_typecheck_baset19do_initializer_listERK5exprtRK5typetb + 1217
7   cbmc                                0x000000010146dd88 _ZN17c_typecheck_baset18do_initializer_recERK5exprtRK5typetb + 184
8   cbmc                                0x0000000101470d7a _ZN17c_typecheck_baset25do_designated_initializerER5exprtR11designatortRKS0_NSt3__111__wrap_iterIPS4_EEb + 4490
9   cbmc                                0x0000000101473e11 _ZN17c_typecheck_baset19do_initializer_listERK5exprtRK5typetb + 1217
10  cbmc                                0x000000010146dd88 _ZN17c_typecheck_baset18do_initializer_recERK5exprtRK5typetb + 184
11  cbmc                                0x000000010146da3e _ZN17c_typecheck_baset14do_initializerER5exprtRK5typetb + 46
12  cbmc                                0x000000010144064d _ZN17c_typecheck_baset23typecheck_expr_typecastER5exprt + 813
13  cbmc                                0x000000010143e179 _ZN17c_typecheck_baset23typecheck_expr_operandsER5exprt + 377
14  cbmc                                0x0000000101439cad _ZN17c_typecheck_baset14typecheck_exprER5exprt + 93
15  cbmc                                0x000000010143e179 _ZN17c_typecheck_baset23typecheck_expr_operandsER5exprt + 377
16  cbmc                                0x0000000101439cad _ZN17c_typecheck_baset14typecheck_exprER5exprt + 93
17  cbmc                                0x0000000101433e7f _ZN17c_typecheck_baset15typecheck_blockER11code_blockt + 79
18  cbmc                                0x000000010142c833 _ZN17c_typecheck_baset23typecheck_function_bodyER7symbolt + 403
19  cbmc                                0x000000010142a5ae _ZN17c_typecheck_baset16typecheck_symbolER7symbolt + 1102
20  cbmc                                0x000000010142eb7a _ZN17c_typecheck_baset21typecheck_declarationER19ansi_c_declarationt + 2154
21  cbmc                                0x000000010141a4ac _ZN17ansi_c_typecheckt9typecheckEv + 60
22  cbmc                                0x000000010194cdfe _ZN10typecheckt14typecheck_mainEv + 62
23  cbmc                                0x000000010141a508 _Z16ansi_c_typecheckR18ansi_c_parse_treetR18symbol_table_basetRKNSt3__112basic_stringIcNS3_11char_traitsIcEENS3_9allocatorIcEEEER16message_handlert + 72
24  cbmc                                0x0000000101416a65 _ZN16ansi_c_languaget9typecheckER18symbol_table_basetRKNSt3__112basic_stringIcNS2_11char_traitsIcEENS2_9allocatorIcEEEEbRKNS2_3setI8dstringtNS2_4lessISC_EENS6_ISC_EEEE + 165
25  cbmc                                0x0000000101416981 _ZN16ansi_c_languaget9typecheckER18symbol_table_basetRKNSt3__112basic_stringIcNS2_11char_traitsIcEENS2_9allocatorIcEEEEb + 33
26  cbmc                                0x000000010186e40d _ZN15language_filest16typecheck_moduleER18symbol_table_basetR16language_moduletbR16message_handlert + 685
27  cbmc                                0x000000010186dfe8 _ZN15language_filest9typecheckER18symbol_table_basetbR16message_handlert + 1960
28  cbmc                                0x0000000101536bf0 _Z28initialize_from_source_filesRKNSt3__14listINS_12basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEENS4_IS6_EEEERK8optionstR15language_filestR13symbol_tabletR16message_handlert + 896
29  cbmc                                0x0000000101537e60 _Z21initialize_goto_modelRKNSt3__16vectorINS_12basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEENS4_IS6_EEEER16message_handlertRK8optionst + 784
30  cbmc                                0x0000000101243bd6 _ZN19cbmc_parse_optionst16get_goto_programER11goto_modeltRK8optionstRK8cmdlinetR19ui_message_handlert + 326
31  cbmc                                0x00000001012426af _ZN19cbmc_parse_optionst4doitEv + 1119
32  cbmc                                0x00000001018e180f _ZN19parse_options_baset4mainEv + 143
33  cbmc                                0x00000001012374d8 main + 40
34  dyld                                0x00007ff8056a2386 start + 1942


--- end invariant violation report ---
[1]    20115 abort      cbmc generic.c

CBMC version: 5.95.1
Operating system: macos
Exact command line resulting in the issue:cbmc main.c
What behaviour did you expect: analysis terminates
What happened instead: cbmc runs forever an consumes 65gigs of ram.