On Mon, Oct 27, 2025 at 1:47 PM Herb Sutter via SG21 <sg21_at_[hidden]>
wrote:

> [adding back sg21]
>
>
>
> Thanks to everyone who responded – I asked for corrections and I meant it
> 😊
>
>
>
> I think we all agree there’s more than one kind of static analysis. As I
> said in my first note, there definitely would also be an analysis that uses
> the contracts to statically detect code paths that could violate contracts;
> we all want that.
>
>
>
> I’ll try again to express a nagging concern about the example:
>
>
>
> > int8_t f(uint32_t i)
>
> > pre(i<128)
>
> > {
>
> > if(i<128)
>
> > return i;
>
> > }
>
>
>
> It’s been suggested that a normal static analysis of the function body
> could assume the precondition is true (e.g., possibly always, possibly only
> when we know we’re in an enforced build), and therefore not warn about the
> missing return paths.
>

I think you're getting hung up on what "normal static analysis" is, and I
don't think there is such a thing. There are different tools that answer
different questions, and they all fit into the software development
lifecycle in different ways.

What I would want static analysis, as a separate tool from the compiler, to
prove for me is "if the preconditions are met then do we violate any other
contract assertions in the body of the function?" Doing that has nothing
to do with what semantic the assertions are evaluated with (unless the
predicate itself alters the answer as a side effect --- in which case, i'd
rather have that told to me as an error.) In general, I don't believe most
static analysis systems will even be able to talk about predicates where
they can't identify that the side effects are nonexistent or not
destructive.

There's another point hidden in my last paragraph --- I would expect each
static analysis tool to have a range of types of predicates it supports,
and thus the question the static analysis tool answers becomes "If you
don't violate a precondition i understand then you won't violate any other
contract assertions i understand". Not being able to check all contract
assertions is a feature, not a bug, and a way for us to get runtime checks
now and a wide range of ever-more-powerful tools in the future.

The utility of answering this question is that building a program from
components where you've answered this question "no, i can't hit other
contract assertions if i satisfy precondtiions" means you won't hit those
contract assertions in the scope in which you've achieved that goal -- and
the larger you make that scope, the closer you are to having eliminated
those bugs for which you've added contract assertions that your particular
tool understands.

Now there's a separate tool where you completely ignore the contract
assertions.... and that's a potentially useful one if you want to start
making guarantees to clients about being well-behaved when they misuse your
functions. But it's a very different tool and is helped much less by
adding the contract assertions in the first place.



> I think what’s bothering me is: Isn’t that bordering on relying on the
> precondition for run-time control flow? I think that what’s triggering me
> because it feels like a category error, but maybe I just don’t
>

"Flow control" would be using the assume semantic for contract assertions
that you've proven to not be violated to your own satisfaction.

What is happening here is managing developer focus --- make sure contract
assertions aren't violated and then you never need to consider the behavior
when the branches where they are violated are taken. If you make a
mistake the program iss still well defined and you can reason about what
happened, but the general solution to such mistakes is not to find the
assertion that was violated and make sure it doesn't' get violated, not to
alter the behavior when there has been a violation that was not detected at
runtime.