CBMC 5.95.1 misses an error for program with cast to pointer

[christina1993]

CBMC 5.95.1 seemingly misses the assertion violation in the following short program that I previously wrote:

#include <assert.h>
int main(){
  char* x = "";
  char* ptr = (char *) 0x55a8a2e6b007;
  assert(ptr != x);
}

When executing cbmc without any options I get:

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing my_test.c
Converting
Type-checking my_test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000705736s
size of program expression: 24 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.4369e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000148792s
Running propositional reduction
Post-processing
Runtime Post-process: 3.892e-06s
Solving with MiniSAT 2.2.1 with simplifier
128 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 1.7748e-05s
Runtime decision procedure: 0.000196021s

** Results:
my_test.c function main
[main.assertion.1] line 6 assertion invalid_char_pt != x4: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

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

[tautschnig]

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.