Memory blowup during typechecking
Opened this issue · 0 comments
remi-delmas-3000 commented
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.