As someone who works on an analysis tool, my approach would probably look like this:

  *
Assuming the boundaries of the contract, is the body correct?
  *
Do any callers violate the contract?
  *
And of course keep checking things that the contract makes no mention of

________________________________
From: SG15 <sg15-bounces_at_lists.isocpp.org> on behalf of Ville Voutilainen via SG15 <sg15_at_[hidden]>
Sent: Monday, October 27, 2025 12:49 AM
To: Joshua Berne <berne_at_[hidden]>
Cc: Ville Voutilainen <ville.voutilainen_at_[hidden]>; sg21_at_[hidden] <sg21_at_[hidden]>; sg15_at_[hidden] <sg15_at_[hidden]>; Tom Honermann <tom_at_[hidden]>
Subject: Re: [isocpp-sg15] [isocpp-sg21] P3835 -- Different contract checking for different libraries

On Mon, 27 Oct 2025 at 03:47, Joshua Berne <berne_at_[hidden]> wrote:
>
>
>
> On Sun, Oct 26, 2025 at 8:37 PM Ville Voutilainen <ville.voutilainen_at_[hidden]> wrote:
>>
>> On Mon, 27 Oct 2025 at 02:24, Joshua Berne <berne_at_notadragon.com> wrote:
>> > There are many ways to analyze code with contracts --- all aided in being more useful because the contracts are actually written out in a way that the tools can understand --- and each way will benefit different users and use cases to different amounts.
>>
>> It seems like there's a very good chance that we can get to a
>> non-violent agreement here.
>
>
> Anything is possible.
>
>
>>
>> Herb's axiom-corollary post is riddled with presumptions of the ilk
>> "this is (the only thing) what static analysis should do, these are
>> the things it can rely on,
>> and then it always does this-and-that".
>>
>>
>> And both of us say "no it isn't".
>
>
> Yup.

Good enough. Now, getting back to Herb's email.. for P2900 contracts,
some parts of your analysis needs to take into account
what happens when those contracts are evaluated with the 'ignore'
semantic, and have to take into account that the behavior
may be different from the case of when they are evaluated with the
'enforce' semantic, and analyze for both cases. The former also
includes cases
where your code might have a redundant check that makes it tolerable
to invoke your functions with preconditions violated,
because such redundant checks are there. It doesn't make those calls
correct, but it makes them tolerable.

But it's not the case that the following is always the case, either:

>A tool that analyzes the non-contract (“ordinary”) code should always analyze the correctness of the body ignoring contracts (or, equivalently, assuming contracts are ignored).

If you always do that, then the tool will tell you that your body
isn't correct unless it has a redundant check. That's different from
analyzing the body 'assuming' that the checks are enforced, because in
that case the tool will not suggest that you should have
a redundant check, it will tell you that your function body is fine
because the enforced precondition means that it doesn't
run into funny UB if the precondition is violated.

Those alternate analyses don't need to be done for assertions that are
guaranteed to be checked and also guaranteed to terminate
when the condition is false. Such assertions actually have an axiom
that they prevent subsequent execution with the condition
violated, and the corollary is that analysis of subsequent (but not
prior, because the violation isn't UB, it just terminates)
can be performed with the knowledge (and not presumption/assumption)
that the condition holds, and always holds,
and no compiler flag will change that.

And those guarantees are so strong that they can be used to optimize
the subsequent code for, always, not just in some cases,
including interprocedurally optimizing the subsequent code after a
call to an inline function having such an assertion in it.

All of which means that if you the programmer can afford using a
guaranteed assertion instead of a flexible one, the analysis
of your code both for humans and tools is simpler.
_______________________________________________
SG15 mailing list
SG15_at_[hidden]
https://lists.isocpp.org/mailman/listinfo.cgi/sg15