pon., 27 paź 2025 o 00:23 Herb Sutter via SG21 <sg21@lists.isocpp.org> napisał(a):

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!

Thanks Herb! This question nails the problem.

I must say I would expect quite the opposite behavior from the tools:

int8_t f(uint32_t i)
pre (i<128)
{
if (i<128)
return i;
}

I agree that the static analysis tool should display the same behavior irrespective of contract semantics. But I would expect that the precondition assertion (as well as any other assertion) separates the program execution into two parts: before and after the assertion. In the "before assertion" part, we do not trust that the program would satisfy the condition so we try to find any indication that the precondition could fail. In the "after assertion" part, I would expect the tool to take for granted that the assertion is satisfied, and look for problems with this assumption in mind.

Meaning that in the case above, the tool would not warn on the missing return on the path that has been excluded by the presence of the precondition assertion (irrespective of the semantic).

Regards,

&rzej;