byte_update against a pointer shouldn't be fatal

[smowton]

This can happen in inaccessible code, so it doesn't seem necessary to kill the whole process.

For example, a program might do something like

f(bool unknown) {
  int i = 0;
  void *ptr = nullptr;
  void *i_or_ptr = unknown ? &i : &ptr;
  if(unknown)
    ((int*)i_or_ptr) = 1;
}

This doesn't do anything unsafe, but symex might produce a byte-update against ptr regardless based on the incorrect assumption that unknown may have changed between lines 4 and 5. Therefore I argue we shouldn't unconditionally reject such an expression.

I raise this now because with #3725 applied we get byte-update expressions against pointers which were previously hidden as byte-extract + with. The meaning of the expression is the same, but it trips this path, indicating the invariant also fails to find all cases where pointers are updated byte-wise.

[tautschnig]

Hmm, maybe I could instead get #4121 reviewed so that I can make progress on #2068 and the PRs I'm factoring out from it? Once #2068 is in we shouldn't have any byte operations on pointers hitting the back-end anymore. Let's please not allow unsoundness creep back in.

[allredj]

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

[smowton]

Marking do not merge on the assumption #2068 makes this redundant

[smowton]

It did indeed