You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Casting an integer to a pointer is implementation-defined behaviour in C. So, yes, it would be great if CBMC considered all possible implementations, but our pointer model doesn't currently do this. We have ideas on how we might fix this, but not clear timeline on when that'll be complete.
CBMC 5.95.1 seemingly misses the assertion violation in the following short program that I previously wrote:
When executing cbmc without any options I get:
0x55a8a2e6b007 is a value I actually encountered for x in a previous run on my machine, so the assertion is indeed unsafe.
Thanks in advance
The text was updated successfully, but these errors were encountered: