C is Brittle D is Plastic

[Richard (Rikki) Andrew Cattermole]

On 09/04/2026 8:34 AM, H. S. Teoh wrote:
> You also don't do actual flow, because that can be arbitrarily complex
> and lead to the halting problem; instead, you do a simplified flow: when
> you encounter an if-statement, you step over both branches and compute
> the value set for both, then at the end you assume the worst case and
> take their union.  Loops are handled the same way: you step through the
> loop body once, then assume the worst and reduce the set only if you're
> able to prove that *every* loop iteration reduces it. If you can't prove
> that, assume the worst and take the unreduced set prior to the loop.
> There may be some simple loops (e.g. foreach) where more advanced
> reasoning can be applied, but basically you apply special cases where
> you can to reduce the value set, and where you can't just assume the
> worst / take the conservative assumption.

You're talking about doing a meet operation on lattices.

Walter knows how to do this, he has implemented this before I was ever born.

However this is the original way, there are other solutions for how to 
handle it now that don't use the meet operation, and instead keep all 
the state around.

But alas more cpu and ram costs.

They could not be implemented in the early 2000's when static analyzers 
surged in implementation and usage.

> Then at the end, if you're able to reduce the set, then the missing
> elements are provably impossible, and you can reason about whether the
> remaining values can possibly overrun bounds.
> 
> But as Rikki said, all of this won't be fast.  And obviously there will
> be cases it cannot catch.  So it's a toss-up whether such a thing is
> worth implementing in a compiler.

After a bit more reading of: 
https://www.nist.gov/publications/sate-vi-report-bug-injection-and-collection

I notice that Frama-C with Eva also meets the sound critera and it is free.