pon., 27 paź 2025 o 00:23 Herb Sutter via SG21 <sg21_at_[hidden]>
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;