Subject: bug#36370: 27.0.50; XFIXNAT called on negative numbers

From: Paul Eggert <[email-masked]>
Date: Fri, 28 Jun 2019 10:46:52 -0700

Pip Cet wrote:
> It's way too easy
> to do something like
> 
> eassume(ptr->field >= 0 && f(ptr));
> 
> when what you mean is
> 
> eassume(ptr->field >= 0);
> eassume(f(ptr));

These mean the same thing. Both tell the compiler that a certain condition (A && 
B) is known to be true, and that behavior is undefined if (A && B) is false. The 
fact that Gnulib+GCC implements them differently is a quality-of-implementation 
issue, not a semantics issue.

> I'm saying that the programmer is
> allowed to assume that the expression passed to assume either has been
> evaluated, or hasn't been, with no in-between interpretations allowed
> to the compiler.

I don't see why that assumption is valid. It's OK if GCC partially evaluates the 
expression. As a silly example, eassume (0 * dump_core () + getchar ()) is not 
required to call dump_core, even if the compiler generates a call to getchar.

Perhaps we should change the comments in verify.h to make this point clearer.