A `might be uninitialized` message after being initialized

[Ganton]

Dear NASA IKOS people,

First of all, thanks your good work.

When people read https://ntrs.nasa.gov/api/citations/20190032510/downloads/20190032510.pdf or https://ntrs.nasa.gov/api/citations/20220007431/downloads/SWS_TC3_IKOS_Tutorial.pdf , tries its example:

    int tab[10];
    for (int i = 0; i < 10; i++) {
        tab[i] = i * i;
    }

and (at the end) adds a simple

    tab[2] = tab[1];

people get a

    warning: expression 'tab[1]' might be uninitialized
    tab[2] = tab[1];

Thanks again for the good work!

[arthaud]

Hi @Ganton,

This is a known limitation of ikos. The uninitialized variable checker can cause many false positives, I usually recommend to disable it.

For more context, this is because ikos uses abstract interpretation under the hood, which enables us to compute an over-approximation of all reachable states. The loop invariant we currently infer is: for all i, tab[i] is either uninitialized or is between [0, 9*9]. When we exit the loop, we are not able to refine that invariant to infer that all elements are initialized. This could be fixed with a custom abstract domain - something called array slicing or array smashing IIRC? For instance, we need to infer that: at iteration i, for all j with 0 <= j < i, tab[j] is initialized so we can infer the right constraint when i = 10 at the end.