NULL compares equal to 0

[tautschnig]

When comparing constants, we just compared their string representations.
This fails when one side of the (in)equality was NULL while the other
side was 0, which is wrong when config.ansi_c.NULL_is_zero is set. Thus
actually test both sides for being zero in this configuration.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 15bf786).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108192432

[kroening]

If config.ansi_c.NULL_is_zero is false, can we really conclude that a non-zero pointer is NOT equal to NULL?

[kroening]

(Very academic question; I am yet to spot a system in which NULL isn't a zero bit pattern).

[tautschnig]

See http://c-faq.com/null/machexamp.html for the discussion of NULL-is-not-zero. But, yes, this remains academic.

[tautschnig]

If config.ansi_c.NULL_is_zero is false, can we really conclude that a non-zero pointer is NOT equal to NULL?

Hmm, indeed, we should probably just refrain from simplifying in that case. Let me fix this.

[tautschnig]

If config.ansi_c.NULL_is_zero is false, can we really conclude that a non-zero pointer is NOT equal to NULL?

Hmm, indeed, we should probably just refrain from simplifying in that case. Let me fix this.

Done.

[tautschnig]

As a side note: a still-current scenario is that the address 0 is a valid place to store data, which is true in about any freestanding setting. There are probably several places where we don't currently account for this in CBMC...

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 7562a99).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108214328

[smowton]

Add a test exercising the !null_is_zero path?

[smowton]

AFAIK unsigned long is the type guaranteed to have same size as a pointer

[tautschnig]

Not on Windows/LLP64... (and also it would be ok for the integer type to be larger than the pointer type in this union, but not the other way around)

[smowton]

Gah, so it isn't, Though perhaps intptr_t is better?

[tautschnig]

Done.

[tautschnig]

Add a test exercising the !null_is_zero path?

Test added!

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 8f68057).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108223887