Bogus warning expression <xx> might be uninitialized

[yurivict]

In this program:

#include <stdio.h>

int a[10];
int main(int argc, char *argv[]) {
    int i = 0;
    for (; i < 10; ++i)
        a[i] = i;
    printf("%i", a[i - 10]);
}

a[i-10] is initialized in the end, but ikos complains that it isn't initialized.

# Results
loop.c: In function 'main':
loop.c:8:5: warning: expression 'a[(int64_t)(i - 10)]' might be uninitialized
    printf("%i", a[i - 10]);
    ^

Version: 3.1
FreeBSD 13.1

[arthaud]

Yes, I have seen this as well.
It's actually hard to prove that a[i] is initialized using abstract interpretation, since we compute an over-approximation of reachable states. We need to infer that the loop actually iterated over all i from 0 to 9, and not just some of them (you could do i+=2).
I think we just disabled the uninitialized variable analysis in the past, but it was re-enabled for @richardlford's work.
Note that you can use -a to run specific analyses or disable others, e.g -a="*,-uva". See README.md

[ivanperez-keera]

I think as of right now there's nothing that needs to be done here. The issue here is that one of ikos' defaults tends to throw many false positives. We either leave it as is (close), document it further, or change the default back.

I'm happy closing this as is and re-visiting it if people keep asking about it.