Pointer to struct with flexible array member as parameter to entry point causes invariant violation

[yumibagge]

CBMC version: 5.12 (cbmc-5.12-d8598f8-953-g7fabc9d69)
Operating system:Ubuntu 18.04.2 LTS
Exact command line resulting in the issue: cbmc flexible_member_array.c --function testFunc
What behaviour did you expect: no invariant violation
What happened instead:invariant violation occurs as follows

Parsing flexible_member_array.c
Converting
Type-checking flexible_member_array
--- begin invariant violation report ---
Invariant check failed
File: /home/diffblue/yumi.bagge/gitrepo/cbmc/src/ansi-c/c_nondet_symbol_factory.cpp:166 function: gen_nondet_array_init
Condition: array_size > 0
Reason: Arrays should have positive size
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4b) [0x119bafb]
cbmc(get_backtrace[abi:cxx11]()+0x43) [0x119c023]
cbmc(_Z29invariant_violated_structuredI17invariant_failedtJRKNSt7__cxx1112basic_stringIcSt11char_traitsIcESaIcEEEEENSt9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES8_S8_iS8_DpOT0_+0x31) [0x9bb8f1]
cbmc() [0x9bb8b3]
cbmc(symbol_factoryt::gen_nondet_array_init(code_blockt&, exprt const&, unsigned long, std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> > const&)+0x330) [0xcee820]
cbmc(symbol_factoryt::gen_nondet_init(code_blockt&, exprt const&, unsigned long, std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> >, bool)+0xd4f) [0xcee16f]
cbmc(symbol_factoryt::gen_nondet_init(code_blockt&, exprt const&, unsigned long, std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> >, bool)+0xc4b) [0xcee06b]
cbmc(symbol_factoryt::gen_nondet_init(code_blockt&, exprt const&, unsigned long, std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> >, bool)+0x4df) [0xced8ff]
cbmc(symbol_factoryt::gen_nondet_init(code_blockt&, exprt const&, unsigned long, std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> >, bool)+0x4df) [0xced8ff]
cbmc(c_nondet_symbol_factory(code_blockt&, symbol_tablet&, dstringt, typet const&, source_locationt const&, c_object_factory_parameterst const&, lifetimet)+0x490) [0xceef80]
cbmc(build_function_environment(std::vector<code_typet::parametert, std::allocator<code_typet::parametert> > const&, code_blockt&, symbol_tablet&, c_object_factory_parameterst const&)+0x215) [0xcdd665]
cbmc(generate_ansi_c_start_function(symbolt const&, symbol_tablet&, message_handlert&, c_object_factory_parameterst const&)+0x331e) [0xce13ee]
cbmc(ansi_c_entry_point(symbol_tablet&, message_handlert&, c_object_factory_parameterst const&)+0x73f) [0xcde0af]
cbmc(ansi_c_languaget::generate_support_functions(symbol_tablet&)+0x4a) [0xce45ea]
cbmc() [0xdef7b8]
cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, message_handlert&, optionst const&)+0x10e3) [0xdee9c3]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0xe6) [0x9c71a6]
cbmc(cbmc_parse_optionst::doit()+0xad7) [0x9c54a7]
cbmc(parse_options_baset::main()+0x639) [0x11c4449]
cbmc(main+0x42) [0x9bab62]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f17738a0b97]
cbmc(_start+0x2a) [0x9baa5a]


--- end invariant violation report ---
[1]    26113 abort (core dumped)  cbmc flexible_member_array.c --function testFunc

input C (initial example was simplified thanks to the review by @danpoe 🙂)

#include <stdlib.h>

typedef struct ST {
	int id;
	int c[];
} ST;

void testFunc(ST ** t) {
}

@hannes-steffenhagen-diffblue is aware of the issue (in fact this is already known issue but we could not find) and I believe he is working on it.