Inconsistent results from pointer comparison

[Anthonysdu]

#include <assert.h>
extern int nondet_int();
int main() {
  int m = nondet_int();
  int *n = &m;
  
  if((unsigned long)n >= (unsigned long)(-4095))
    assert((unsigned int)(-1 * (long)n) < 6);
    
  int a = -2048;
  if((unsigned long)a >= (unsigned long)(-4095))
    assert((unsigned int)(-1 * (long)a) < 6);
}

** Results:
main.c function main
[main.assertion.1] line 8 assertion (unsigned int)(-1 * (long)n) < 6: SUCCESS
[main.assertion.2] line 12 assertion (unsigned int)(-1 * (long)a) < 6: FAILURE

** 1 of 2 failed (2 iterations)

Hi, is there a problem here in the first assertion? it should fail if n = -2048.

[tautschnig]

In C, pointer-to-integer conversion is implementation-defined behaviour. That should give CBMC the freedom to choose an implementation where the condition (unsigned long)n >= (unsigned long)(-4095) never evaluates to true.

It is, however, also right to argue that CBMC should seek to model all possible implementations. The pointer-to-integer conversion in CBMC does not currently fulfil this expectation, but we will hopefully fix this in future.