goblint
Remove division by zero error message during base `invariant`
Discovered in https://github.com/goblint/analyzer/pull/1838#discussion_r2571447038. Should be redundant due to #1764. Especially because this only trigger for must division by zero, not may.
It's strange because it's the only warning/error emitted during base invariant.
TODO
- [ ] Is the top-ification even necessary/useful then?
What would you propose instead of top? Raising deadcode? These seem to be the only sensible things we can do.
(The warning should more likely be an internal analyzer warning, I guess it can sometimes happen that during refinement of something that is actually not reachable we produce some kind of nonsensical value.)
What would you propose instead of
top? Raising deadcode? These seem to be the only sensible things we can do.
I haven't yet thought about what exactly this is trying to achieve, but only top-ifying must zero is odd: [0,0] goes to top, but [0,1] remains [0,1] instead of also going to top for including the problematic 0.
It's the same kind of strangeness that used to be in the interval division: https://github.com/goblint/analyzer/pull/1804#discussion_r2276158981.