refactor(region): add a constraint for size ghost if ref is null ptr

[LinerSu]

We can also improve the precisons if a given reference constraints is p == NULL. For instance,

int sz = int_nd();
__CRAB_assume(sz >= 0);
__CRAB_assume(sz < 10);
uint8_t *ptr = (sz == 0) ? NULL : malloc(sizeof(uint8_t) * sz);

We should expect the post invariants (by zones) for ptr is:

sz -> [0, 9] && ptr.address -> [0, +oo]  && sz <= ptr.address + 8 && ptr.offset == 0 && ptr.size == sz

Or we can do better if we use the polyhedra domain:

sz == ptr.size && -sz <= 0 && sz <= 9 && sz-9*ptr.address <= 0; ; ptr.offset == 0