Remove warn_and_top_on_zero from BaseInvariant for division by zero

[sim642]

This is the continuation of #1892 regarding the top-ification aspect.

I tried to just remove it and no tests fail. But I'll see on sv-benchmarks if this actually matters sometime.

Question

In #1892 (comment):

Okay, so here specifically the question is what the backward transfer function should be for c = a / [0;0], given some value for c, how can one refine a? And what about c = a / [0;1]...

The strange thing is that the warn_and_top_on_zero code is about the second argument, not the first one.

And it looks like it just tries to avoid a definite division by zero in the calculations that follow, e.g. ID.div a b. But doing so isn't actually a problem: once we're doing the refinement, we've already forward-evaluated that exact calculation with the zero divisor without issues. I don't think the abstract division operator in int domains should fail because of that.
Also note that the second argument (without top-ification) would still be, e.g., [0,0], not bottom. So it's not triggering ArithmeticOnIntegerBot by doing that.

Maybe some git archeology is needed for this code. Perhaps it was added at a time when the division operators in int domains had problems with doing this and warn_and_top_on_zero was added to work around them.

TODO

• sv-benchmarks

[sim642]

Maybe some git archeology is needed for this code. Perhaps it was added at a time when the division operators in int domains had problems with doing this and warn_and_top_on_zero was added to work around them.

This is essentially reverting ae01aba. Its previous commit added the following test:

analyzer/tests/regression/27-inv_invariants/02-bot-during-condition.c

Lines 4 to 11 in df5edaa

	int tmp;
	int p_9 = 60;
	tmp = (p_9 +1) % 0;
	if ((p_9 +1) % 0) {
	tmp = 1;
	}

The test doesn't contain any checks though. But it's also not crashing after the revert.