Add proper handling of integer-overflows

[jerhard]

In order to implement proper handling of integer overflows in the analyzed C code, and to be able to deal with values outside the range of OCaml-int64 (#120), we have to make several changes to the integer domains.

1. Add ikind information to the integer domains.
2. Use arbitrary precision integers in the implementation of the domains.
3. In the implementation of the abstract operations of the integer domains, add detection & handling of overflows.

Regarding 1., I added an functor IntDomLifter, that takes a module of signature IntDomain.S and adds a layer to store the ikind.

TODOs:

• it is not clear how the top and bot should look like in the IntDomLifter. These either would have to be of some arbitrary ikind or some additional Top and Bottom element
• 2 and 3. still have to be implemented

[vogler]

Instead of copying module type S to module type Z, it'd be better to just include the common values.

[vogler]

Instead of carrying ikind around we could add it as an argument for operations. Adding an indirection and additional 64 bit for ikind for every abstract int might be costly.
Since a lot of bot/top handling is shared, it's maybe a good idea anyway to merge operations into an unop/binop which gets the operation and ikind.
If we still want to keep the specialized functions like add, sub etc., they could be added by some functor.

[jerhard]

Instead of carrying ikind around we could add it as an argument for operations.

I think there are places besides the arithmetic operations where we want to know the ikind. E.g. if we perform a widen on ints, it would be useful to know what the ikind of the integers is that is being widened.

[michael-schwarz]

This causes sv-comp/sv-benchmarks/c/loops/linear_search.c to unsoundly claim that the error is not reached.
Edit: This seems to be UB in the benchmark, see sosy-lab/sv-benchmarks#1241

[michael-schwarz]

I pushed a problematic example where the ikinds don't line up:

    signed char* s = malloc(10*sizeof(signed char));
    s[0] = -5;

    unsigned char* us = s;
    *us = 12;

This is valid C, and GCC also doesn't complain, but we currently fail with - Fatal error: exception Failure("ikinds signed char and unsigned char are incompatible. Values: (-5) and (12)")

This is this issue we discussed where it would be necessary to go to supertop for Int of different ikind.