[Herb]

  * Axiom: A fundamental property of contracts is that they are redundant - they never change the meaning of code.

What happens when the axiom doesn't reflect the reality of software practice?

-- Gaby

From: SG15 <sg15-bounces_at_[hidden]> On Behalf Of Herb Sutter via SG15
Sent: Sunday, October 26, 2025 4:23 PM
To: sg21_at_[hidden]
Cc: Herb Sutter <herb.sutter_at_[hidden]>; 'Tom Honermann' <tom_at_[hidden]>; 'ISO C++ Tooling Study Group' <sg15_at_[hidden]>
Subject: Re: [isocpp-sg15] [isocpp-sg21] P3835 -- Different contract checking for different libraries


Jonas, thank you for the excellent example.



I think labels can do whatever is wanted here, so my response below has nothing to do with labels... I have a more fundamental question about what tools _should_ do with contracts in such an example, because I think it illustrates how contracts interact with static analysis...



> This is also a tooling issue.

> With a annotated contract a compiler or analyzer can easily issue useful

> diagnostics

>

> int8_t f(uint32_t i)

> pre(i<128)

> {

> if(i<128)

> return i;

> }

>

> If I used a "pre always" the tool should issue a warning "condition always

> true"

> If I used a "pre maybe" the tool should issue a warning "missing return"

>

> This may seem like obvious warnings



That's actually not my understanding of what tools should do. Let me explain why, and would you (and others who know contracts and static analysis better than I do) please correct me and point out where I'm making a mistake:



Axiom: A fundamental property of contracts is that they are redundant - they never change the meaning of code.



Corollary: A program that runs successfully with contracts enforced should also run with the same meaning with contracts ignored. (From this comes "assertions should not have side effects" which is taught in every assertion facility in every language I know of.)



Corollary: 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).



So in the above example, I would expect:



(1) A tool that analyzes the function body would _always_ issue a "does not return on all paths" warning (and all compilers do: https://godbolt.org/z/TebeM1cdc). To silence the warning, add "else std::abort()" "else throw something{};" or or similar. This is right, because the function can indeed be called out of contract, and if so cannot just fall off the end.



(2) A (possibly different) tool that also analyzes contracts would _additionally_ issue a warning if it discovers code paths that would violate the precondition. Contract-related warnings are purely in addition to, not instead of and not interacting with, other warnings.



Jonas, and contract / static analysis experts: Am I on the right track, or did I make a mistake?

Corrections welcome!



Herb