Invariant violation in pointer validity check #8700
Description
This reduced program
int (*a)[];
void b() { *a; }triggers the following invariant violation on f7cd7db898c0a4571071610788ca4e3219b6c996
Generic Property Instrumentation
--- begin invariant violation report ---
Invariant check failed
File: /home/guedemann/source/git/SV/cbmc/src/ansi-c/goto-conversion/goto_check_c.cpp:1470 function: pointer_validity_check
Condition: size_of_expr_opt.has_value()
Reason: Check return value
Backtrace:
cbmc(+0xa7d4a3) [0x577e7d63f4a3]
cbmc(+0xa7e5c3) [0x577e7d6405c3]
cbmc(+0x180a42) [0x577e7cd42a42]
cbmc(+0x7a5d65) [0x577e7d367d65]
cbmc(+0x7a9471) [0x577e7d36b471]
cbmc(+0x7ad937) [0x577e7d36f937]
cbmc(+0x7ae260) [0x577e7d370260]
cbmc(+0x7ae301) [0x577e7d370301]
cbmc(+0x6be027) [0x577e7d280027]
cbmc(+0x182e09) [0x577e7cd44e09]
cbmc(+0x183c26) [0x577e7cd45c26]
cbmc(+0x186e4d) [0x577e7cd48e4d]
cbmc(+0x17ec5b) [0x577e7cd40c5b]
cbmc(+0x170978) [0x577e7cd32978]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x71a08422a1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x71a08422a28b]
cbmc(+0x17ff25) [0x577e7cd41f25]
--- end invariant violation report ---
There are related issues #5293 and #4930 which are marked as resolved but the fix does not seems to cover the above case.