Mixed non-null/maybe-null malloc semantics in a same program

[nunoplopes]

Example from @aqjune so we don't forget:

p = malloc(4)
q = malloc(4)
*p = 10
// can't remove this check
if (q == null) return 1;
*q = 20;
return 2;

=>

p = malloc(4)
q = malloc(4)
*p = 10
*q = 20;
return 2;

always succeed semantics: transformation correct
non-det null semantics: correct, as p is dereferenced

Our model assumes the program uses one model consistently, while the program above mixes models.

1. Do we care about this example?
2. If so, what's the fix? Synchronize mallocs between src/tgt?