I.7: State postconditions - undefined behavior in first "consider using"

The solution to the first example is:

int area(int height, int width)
{
    auto res = height*width;
    Ensures(res>0);
    return res;
}

When the multiplication overflows, undefined behavior is invoked. This makes the Ensures(res>0) depend on undefined behavior.

I'm not sure what the correct solution should be like. Possibly something like clang's and gcc's __builtin_sadd_overflow or one of the techniques described in the book Hacker's Delight. The former would be clang/gcc-specific, the latter quite involved.