Hello,
On Mon, 8 Sep 2025, Iain Sandoe wrote:
> > I have
> > no idea how they'd be actually implemented, so I can't say if it's sensible
> > for those.
>
> (for pre-conditions) they lower to a series of statements like
> if (some check fails)
> handle the contract violation
> if (some other check fails)
> handle the contract violation
> …
>
> > The only "example" is for in(p) in (*p > 5) where the contract
> > *p > 5 would "elide" the 'p' one. Whatever "eliding" means here.
>
> So, IIRC, the argument was
>
> *p > 5 would be UB for p == nullptr
>
> therefore an earlier check for p == nulptr can be removed, because
> that case cannot happen in a well-formed program.
>
> However, that prevents the contract check from doing its job (diagnosing
> the bad case).
But it would also be an invalid transformation of the compiler. So I
can't quite see the worry. The second check ("*p > 5") is conditional on
the first one:
if (!p)
fail()
if (*p > 5)
fail2()
The *p access would only be unconditional if fail() can fall-through.
Two cases:
(a) the spec of contracts says that later contracts may depend on earlier
contracts to have succeeded (dependend contracts): the fail() must not
fall through, that would be an invalid implementation of contracts,
and the compiler removing the first !p check would be buggy
(b) the spec of contracts say that all of them are independend: then
fail() can fall through and the compiler may indeed remove the !p
check (if fail() itself doesn't have any interesting side-effects).
But then the author who wrote those two contracts independendly, where
in reality one depends on the other, was wrong.
In both cases I don't see how an observably_checkpoint facility would
help.
So, again, a precise spec of the supposed semantics of the builtin are
required. Up to now it seems fairly fuzzy and all cases I've seen in this
thread are trying to work around clear compiler or user bugs.
So, what is or isn't guaranteed by the builtin?
Ciao,
Michael.
