CBMC dumps core on simple program

[danielsn]

#include <assert.h>
#include <stddef.h>

struct foo {
  int x;
  int y;
};


int main(struct foo* p)
{
}

CBMC version: 5.12 (cbmc-5.12.1)
Operating system: osx
Exact command line resulting in the issue: cbmc test.c
What behaviour did you expect: no crash. Perhaps an error message
What happened instead:

CBMC version 5.12 (cbmc-5.12.1) 64-bit x86_64 macos
Parsing be.c
Converting
Type-checking be
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20200620-32000-1h7ts1b/src/ansi-c/ansi_c_entry_point.cpp:476 function: generate_ansi_c_start_function
Condition: false
Reason: Unreachable
Backtrace:
0   cbmc                                0x00000001007bb91a _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x00000001007bbdd9 _Z13get_backtracev + 167
2   cbmc                                0x00000001005e9e9c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   cbmc                                0x00000001007cc459 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   cbmc                                0x00000001004f8813 _Z30generate_ansi_c_start_functionRK7symboltR13symbol_tabletR16message_handlertRK28c_object_factory_parameterst + 7689
5   cbmc                                0x00000001004f67ff _Z18ansi_c_entry_pointR13symbol_tabletR16message_handlertRK28c_object_factory_parameterst + 993
6   cbmc                                0x000000010078f0d3 _ZN15language_filest26generate_support_functionsER13symbol_tablet + 135
7   cbmc                                0x00000001005c01f5 _Z21initialize_goto_modelRKNSt3__16vectorINS_12basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEENS4_IS6_EEEER16message_handlertRK8optionst + 2277
8   cbmc                                0x00000001003a0f54 _ZN19cbmc_parse_optionst16get_goto_programER11goto_modeltRK8optionstRK8cmdlinetR19ui_message_handlert + 124
9   cbmc                                0x000000010039fa42 _ZN19cbmc_parse_optionst4doitEv + 958
10  cbmc                                0x00000001007d0716 _ZN19parse_options_baset4mainEv + 136
11  cbmc                                0x0000000100397d7a main + 42
12  libdyld.dylib                       0x00007fff6c537cc9 start + 1
13  ???                                 0x0000000000000002 0x0 + 2


--- end invariant violation report ---

[danielsn]

@danpoe

[hannes-steffenhagen-diffblue]

Cause:

CBMC assumes that functions called main have one of the signatures specified in the C standard (+ a GNU C one that also takes envp), and this isn’t one of them.

Short term remedy:

Fail with a user-friendly error message saying what’s the actual problem.

Potential alternative:

Treat main with a nonstandard signature as a regular entry point. Problem with that is that we special case some of them, so when using another signature a user might have a different special case in mind which we would silently ignore.

[hannes-steffenhagen-diffblue]

@danielsn With #5416 we consider this done for now, unless support for specific nonstandard signatures is needed in which case we should track it as another issue.