Improve the value domain to keep track of integer sets

[arthaud]

On the following code:

int main() {
    const int indexes[5] = {2, 0, 4, 1, 3};
    int array[5];

    for (int i = 0; i < 5; i++) {
        int index = indexes[i];
        array[index] = index;
    }

    return 0;
}

IKOS produces the following warning:

test.c:7:22: warning: possible buffer overflow, could not bound index for access of local variable 'array' of 5 elements
        array[index] = index;
                     ^

To remove this warning, the analysis needs to bound all the integers stored in the indexes array. It could infer that indexes[i] is in [0, 4] and prove that the array access is safe.

[arthaud]

This could be implemented in the memory domain by adding a map from memory locations to a value set abstraction.

This is already implemented for pointers with the _pointer_sets map.

This false positive appears in our benchmarks:

• 2 times in aeroquad
• 5 times in gen2