Is there no tool out there that can analyze code under the assumption that
contracts will hold? And then possibly another tool that will exhaustively
analyze possible code flows to verify that assumption?

On Mon, Oct 27, 2025 at 9:49 AM Ville Voutilainen via SG21 <
sg21_at_[hidden]> wrote:

> 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_[hidden]>
> 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.
> _______________________________________________
> SG21 mailing list
> SG21_at_[hidden]
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
> Link to this post: http://lists.isocpp.org/sg21/2025/10/11775.php
>