Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

On Wed, 16 Jan 2019 at 14:29, James Coleman <jtc331(at)gmail(dot)com> wrote:
>
> On Tue, Jan 15, 2019 at 8:14 PM David Rowley
> > While int4pl might do what you want, some other strict function might
> > not. A simple example would be a strict function that decided to
> > return NULL when the two ints combined overflowed int.
>
> Yes, the claim about not all strict functions guarantee this (like
> int4pl) made sense.
>
> Is your preference in this kind of case to comment the code and/or
> tests but stick with int4pl even though it doesn't demonstrate the
> "problem", or try to engineer a different test case such that the
> *_holds results in the tests don't seem to imply we could prove more
> things than we do?

I think using x+x or whatever is fine. I doubt there's a need to
invent some new function that returns NULL on non-NULL input. The
code you're adding has no idea about the difference between the two.
It has no way to know that anyway.

--
David Rowley http://www.2ndQuadrant.com/
PostgreSQL Development, 24x7 Support, Training & Services