CBMC 5.94 now crashes on previously working example

[rod-chapman]

CBMC 5.94 (macOS on Apple Silicon M1) now crashes on a small example that I previously wrote.
This code:
https://github.com/rod-chapman/cbmc-examples/tree/main/ub

I now get:

rodchap@f4d4889dcf6d ub % make
goto-cc --function ub1_harness -DCBMC -o ub1.goto ub1.c
goto-instrument --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --dfcc ub1_harness --apply-loop-contracts --enforce-contract ub1 ub1.goto ub1_contracts.goto
Reading GOTO program from 'ub1.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Contract 'ub1' not found, deriving empty pure contract 'contract::ub1' from function 'ub1'
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'ub1_harness'
Wrapping 'ub1' with contract 'ub1' in CHECK mode
Instrumenting 'printf'
file <builtin-library-printf> line 20 function printf: dfcc_instrument::instrument_other: statement type 'printf' is not supported, analysis may be unsound
Instrumenting 'malloc'
Instrumenting 'free'
Instrumenting '__swbuf'
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20231012-8056-wjuy6q/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp:330 function: instrument_function
Condition: Precondition
Reason: found != goto_model.goto_functions.function_map.end()
Backtrace:
0   goto-instrument                     0x000000010261b06c _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 120
1   goto-instrument                     0x000000010261b3bc _Z13get_backtracev + 44
2   goto-instrument                     0x000000010269cb3c _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 60
3   goto-instrument                     0x000000010220f860 _Z24report_invariant_failureIJNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEEEEvRKS6_S8_iS6_S6_DpOT_ + 84
4   goto-instrument                     0x000000010221c19c _ZN16dfcc_instrumentt19instrument_functionERK8dstringt24dfcc_loop_contract_modetRNSt3__13setIS0_NS4_4lessIS0_EENS4_9allocatorIS0_EEEE + 488
5   goto-instrument                     0x0000000102210b38 _ZN5dfcct26instrument_other_functionsEv + 176
6   goto-instrument                     0x000000010220ead0 _ZN5dfcct20transform_goto_modelEv + 80
7   goto-instrument                     0x000000010220e990 _ZN5dfcctC2ERK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalINSt3__14pairIS5_S5_EEEEbRKNSB_3mapIS5_S5_NSB_4lessIS5_EENSB_9allocatorINSC_IS6_S5_EEEEEE24dfcc_loop_contract_modetR16message_handlertRKNSB_3setINSB_12basic_stringIcNSB_11char_traitsIcEENSK_IcEEEENSI_ISY_EENSK_ISY_EEEE + 404
8   goto-instrument                     0x000000010220e768 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalINSt3__14pairIS4_S4_EEEEbRKNSA_3mapIS4_S4_NSA_4lessIS4_EENSA_9allocatorINSB_IS5_S4_EEEEEEbbRKNSA_3setINSA_12basic_stringIcNSA_11char_traitsIcEENSJ_IcEEEENSH_ISU_EENSJ_ISU_EEEER16message_handlert + 112
9   goto-instrument                     0x000000010220e07c _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalIS4_EEbRKNSt3__13setIS4_NSD_4lessIS4_EENSD_9allocatorIS4_EEEEbbRKNSE_INSD_12basic_stringIcNSD_11char_traitsIcEENSH_IcEEEENSF_ISQ_EENSH_ISQ_EEEER16message_handlert + 304
10  goto-instrument                     0x0000000102278560 _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 5196
11  goto-instrument                     0x0000000102274a74 _ZN30goto_instrument_parse_optionst4doitEv + 552
12  goto-instrument                     0x0000000102642fe8 _ZN19parse_options_baset4mainEv + 180
13  goto-instrument                     0x00000001021dda78 main + 48
14  dyld                                0x000000018d057f28 start + 2236

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
Function '__swbuf' must exist in the model.
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
make: *** [ub1_contracts.goto] Abort trap: 6

[remi-delmas-3000]

With CBMC 5.94.0 I can see that the goto-binary produced by goto-cc declares a function symbol __sputc and a function symbol __swbuf,

The GOTO function for __sputc calls __swbuf but we have no goto function for __swbuf.

None of these functions are reachable from the entry point though. They must be dependencies of printf but printf itself is stubbed out by the CPROVER version and shallow.

Adding a pass with goto-instrument --drop-unused-functions before applying contracts solves the problem, but goto-cc should maybe try to get rid of __sputc from the start

[tautschnig]

I am not entirely sure this is a new feature of CBMC, but it might rather be a symbol dragged in by the C library on macOS? Perhaps 0de2cb1 needs to take higher priority, and we should also remove the #ifdef __FreeBSD__?