Void pointer argument cannot be pointer-checked

[xbauch]

#include <assert.h>

void foo(void *arg)
{
  assert(*(unsigned *)(arg) == 5);
}

CBMC version: 5.12 (cbmc-5.12-d8598f8-552-g03cc69c04-dirty)
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: $ cbmc main.c --function foo --pointer-check
What behaviour did you expect: VERIFICATION FAILED
What happened instead:

--- begin invariant violation report ---
Invariant check failed
File: /home/diffblue/petr.bauch/code/cbmc/src/analyses/goto_check.cpp:1116 function: pointer_validity_check
Condition: size_of_expr_opt.has_value()
Reason: Check return value
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4d) [0x55c5af45da7a]
cbmc(get_backtrace[abi:cxx11]()+0x45) [0x55c5af45dc81]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x4e) [0x55c5aed83491]
cbmc(+0x711c3d) [0x55c5aed82c3d]
cbmc(goto_checkt::pointer_validity_check(dereference_exprt const&, exprt const&, guard_exprt const&)+0x17b) [0x55c5aeff43eb]
cbmc(goto_checkt::check_rec(exprt const&, guard_exprt&)+0x654) [0x55c5aeffa79a]
cbmc(goto_checkt::check(exprt const&)+0x6a) [0x55c5aeffa820]
cbmc(goto_checkt::goto_check(dstringt const&, goto_functiont&)+0xb0f) [0x55c5aeffb9e9]
cbmc(goto_check(namespacet const&, optionst const&, goto_functionst&)+0xec) [0x55c5aeffd7a4]
cbmc(goto_check(optionst const&, goto_modelt&)+0x55) [0x55c5aeffd85f]
cbmc(cbmc_parse_optionst::process_goto_program(goto_modelt&, optionst const&, messaget&)+0x310) [0x55c5aed8cff4]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x15d) [0x55c5aed8c773]
cbmc(cbmc_parse_optionst::doit()+0x747) [0x55c5aed8afe9]
cbmc(parse_options_baset::main()+0x114) [0x55c5af4825c2]
cbmc(main+0x55) [0x55c5aed8292f]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f96e7d0fb97]
cbmc(_start+0x2a) [0x55c5aed827fa]


--- end invariant violation report ---

[tautschnig]

Closing as the issue was resolved in b8f6483 (#5427).