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.
