Bounds widening for _Nt_array_ptr's

[mgrang]

_Nt_array_ptr's are terminated by a null terminator. If we determine that the dereference of a _Nt_array_ptr is non-null then we can widen the bounds of the pointer by 1 because there will always be at least the null terminator in the string.

Formally we can state the problem as:
∀ p | p ∈ _Nt_array_ptr & bounds(p) = [l, u)
*p != 0 => bounds(p) = [l, u + 1)

Example:
_Nt_array_ptr<char> p : count(0) = "abc"; // bounds = [0, 0]
if (*p) { // bounds = [0, 1) }