Address domain bucket conflict with first field offset

[sim642]

This is an issue which wouldn't be fixed by #967 and occurs in brubeck of goblint/bench#53.

An Lattice.Uncomparable exception is raised from the joining of offsets (last case):

analyzer/src/cdomains/lval.ml

Lines 127 to 138 in 7f7b9f0

	let rec merge cop x y =
	let op = match cop with `Join -> Idx.join | `Meet -> Idx.meet | `Widen -> Idx.widen | `Narrow -> Idx.narrow in
	match x, y with
	| `NoOffset, `NoOffset -> `NoOffset
	| `NoOffset, x
	| x, `NoOffset -> (match cop, cmp_zero_offset x with (* special cases not used for AddressDomain any more due to splitting *)
	| (`Join | `Widen), (`MustZero | `MayZero) -> x
	| (`Meet | `Narrow), (`MustZero | `MayZero) -> `NoOffset
	| _ -> raise Lattice.Uncomparable)
	| `Field (x1,y1), `Field (x2,y2) when CilType.Fieldinfo.equal x1 x2 -> `Field (x1, merge cop y1 y2)
	| `Index (x1,y1), `Index (x2,y2) -> `Index (op x1 x2, merge cop y1 y2)
	| _ -> raise Lattice.Uncomparable (* special case not used for AddressDomain any more due to splitting *)

The comment claims that the case is no longer used with buckets, but turns out it may be.

In particular, consider the join of bucketed address sets

((alloc@sid:628@tid:[main](#top)), concrat/brubeck/main.c:1841:3-1841:12).sampler ->
	((alloc@sid:628@tid:[main](#top)), concrat/brubeck/main.c:1841:3-1841:12).sampler

and

((alloc@sid:628@tid:[main](#top)), concrat/brubeck/main.c:1841:3-1841:12) ->
	((alloc@sid:628@tid:[main](#top)), concrat/brubeck/main.c:1841:3-1841:12).backend

The offset join is called on .sampler and .backend when the buckets are being merged.

This is surprising because the keys (representatives) of the buckets appear different: one has no offset and the other has .sampler.
Although the address sets buckets intend for them to be separate, the equality of offsets still uses the old special-cased logic:

analyzer/src/cdomains/lval.ml

Lines 92 to 105 in 7f7b9f0

	let rec compare o1 o2 = match o1, o2 with
	| `NoOffset, `NoOffset -> 0
	| `NoOffset, x
	| x, `NoOffset when cmp_zero_offset x = `MustZero -> 0 (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *)
	| `Field (f1,o1), `Field (f2,o2) ->
	let c = CilType.Fieldinfo.compare f1 f2 in
	if c=0 then compare o1 o2 else c
	| `Index (i1,o1), `Index (i2,o2) ->
	let c = Idx.compare i1 i2 in
	if c=0 then compare o1 o2 else c
	| `NoOffset, _ -> -1
	| _, `NoOffset -> 1
	| `Field _, `Index _ -> -1
	| `Index _, `Field _ -> 1

Thus, when the maps are being joined, the keys are found to be equal and hence their values are attempted to be joined.

Therefore, to fix the issue, the special cased logic should be stripped out completely (which #967 does not yet do!).