As a developer of static analysis, I can state the following:

  *
I'm not trying to prove anything, however nice that would be. Proving almost anything in the presence of pointers or loops is largely impossible (see Rice's theorem).
  *
Given the above, I don't really care if your predicate looks like it might have a side effect. I'm going to assume it does not. Proving the presence of absence of side effects is again largely impossible in the presence of pointers.
  *
Contracts would still be useful, by providing conditions that might not be obvious or possible to infer from the implementation, as well as making reports more local
  *
I would not care whether contracts are meant to be enforced or not. Contract violations are expected to be a bug in the caller. There is indeed a bit of a philosophical argument about whether seeming logical errors in the implementation of a function (such as the missing return example given) should be ignored because a contract prevents them. I would lean towards "do not report", notably because it's unclear what's a good way to fix such issues. Adding an abort in the example seems overkill, just like you wouldn't add an aborting null check on a dereference of a pointer that's contract-checked to be non-null. But that can also just be configurable.

________________________________
From: SG15 <sg15-bounces_at_[hidden]> on behalf of Joshua Berne via SG15 <sg15_at_[hidden]>
Sent: Monday, October 27, 2025 11:07 AM
To: sg21_at_[hidden] <sg21_at_[hidden]rg>
Cc: Joshua Berne <berne_at_[hidden]>; sg15_at_lists.isocpp.org <sg15_at_[hidden]>
Subject: Re: [isocpp-sg15] [isocpp-sg21] P3835 -- Different contract checking for different libraries



On Mon, Oct 27, 2025 at 1:47 PM Herb Sutter via SG21 <sg21_at_[hidden]<mailto: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.