Semantics of __VERIFIER_nondet_pointer

Currently the semantics of __VERIFIER_nondet_pointer are not fully clear.

Open questions:

• Does this method potentially allocate new memory?
• Can resulting pointers be passed to free?

It was discussed (#745, #750) whether __VERIFIER_nondet_pointer could be completely replaced by calls to other functions like __VERIFIER_nondet_ulong, but there are problems with that:

• Size of pointer is architecture-dependent, so any replacement would need to be specific per architecture (error-prone).
• Pointers need to be correctly aligned, and a simple call to __VERIFIER_nondet_ulong would not guarantee this.

Thus we should keep __VERIFIER_nondet_pointer and define it properly. I suggest the following guarantees should be part of the definition:

• Result is 0 or a valid pointer.
• Result is correctly aligned for all types on the architecture (like the result of malloc).

Of course the open questions still need to be decided on, and probably we need to make this definition more precise.