Remove custom octagon analysis, make Apron Analysis answer MustBeEqual, MayBeEqual, and MayBeLess queries

[jerhard]

As we have working Apron bindings, the custom implemented octagon analysis is now superfluous. Also, the OctagonAnalysis did not take different ikinds of integers into account, and was coupled with some parts of IntDomain, making changes there more costly to do.

Part of #460.

[jerhard]

The test 23/13-advantage_for_last.c for was annotated to use octagons but didn't need them, so I simply removed the option annotation.

There were two other tests for the octagon analysis together with partitioned arrays ("22/10 array_octagon", "23/10 array_octagon" ) and copies of these for the precision adaption ("42/14 22_10-array_octagon", "42/20 23_10-array_octagon"). I changed the test cases to use the Apron analysis instead of the Octagon analysis, but these test cases fail now due to imprecision.

[jerhard]

Interestingly, the assert in line 56 fails, while the asserts in lines 54, 55 succeed, and the partitioned array knows that it is partitioned by j, and that the left part of the array has value 1, and the middle part has value 2. Maybe the apron analysis is somehow not queried by the partitioned arrays/the apron analysis does not answer?

analyzer/tests/regression/22-partitioned_arrays/10-array_octagon.c

Lines 49 to 56 in c88666e

	z = j;
	// Values that may be read are 1 or 2
	assert(a[z] == 1); //UNKNOWN
	assert(a[z] == 2); //UNKNOWN
	assert(z >= 0);
	assert(z <= j);
	assert(a[z] == 0); //FAIL

[jerhard]

I would suggest to annotate the tests in question with SKIP and create a separate issue about these. Any objections?

[sim642]

I think the octagon analysis answers queries like MustBeEqual which partitioned arrays use, but the apron analysis doesn't implement them. It shouldn't be too hard to add support for them though.

[jerhard]

@sim642 I extended the apron analysis to also answer the MustBeEqual, MayBeEqual and MayBeLess queries.
Most asserts in the both test cases now work, except for a few. And some asserts now can be shown that previously couldn't.

[sim642]

Maybe @michael-schwarz knows what aspects the octagon analysis had that the apron analysis doesn't that it's not precise enough for that. Did the octagon analysis have something very specific for the partitioned arrays or maybe it was just more precise because it was unsound?

[michael-schwarz]

Did the octagon analysis have something very specific for the partitioned arrays or maybe it was just more precise because it was unsound?

No, it did not have anything very specific. I think it completely ignored overflows, so maybe that is why?