On Mon, 27 Oct 2025 at 01:34, Ville Voutilainen
<ville.voutilainen_at_[hidden]> wrote:
> > 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).
>
> ..seriously wondering what the goal of such a tool is. "I looked for
> bugs in your code and presumed a whole bunch of things,
> and based on those presumptions I came to the conclusion that your
> code doesn't have bugs."

..and more seriously wondering where that "always" came from. If you have

void f(int x) pre(x >= 0)
{
    f1(x);
    f2(x);
    f3(x);
    f4(x);
}

and f1/f2/f3/f4 have preconditions, not necessarily same ones as f
itself, I need the static analyzer to tell me whether
that code is correct. How does it do that ignoring contracts? The
whole point of those contracts would be to tell the analyzer
things that can help its analysis.

And it's not useful to do that analysis ignoring the run-time effects
of the contracts either. I need that analyzer to tell me what
my program does, and whether that's correct. Not to presume that all
contracts in it are correct. I need it to tell me what
my program does when those contracts are enforced, I need it to tell
me what my program does when those contracts are observed.
Because I might run my programs both ways, or all three ways.

If the only thing that the the analyzer tells me is that the program
is platonically correct, but the program then does the wrong thing
when I run
it, that's the end of my use of that analyzer.

Which takes us squarely to the conundrum mentioned in my paper about
this. If the contracts are just plain code, you need to analyze
that code, too. Adding more code to help analyze other code doesn't
magically make it easier to figure out whether the code without the
newly-added
plain code is correct, it makes it harder, especially when the
newly-added code has four different ways it can be run, and any of
those
calls to f1/f2/f3/f4 can be run in any combinations of those ways.

Saying that such newly-added arbitrary code "lights up static
analysis" is a mythconception.