I don't know how a static analyzer could do this:
size_t i = some_function(); // gets return value from environment
array[i] = 3;A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bounds. It is called sound because the absence of a complaint means it has proven the absence of the issues it is meant to catch.
If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.
Nearly all my use of arrays is arrays whose length cannot be known until runtime.
Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones.
At least, that is the theory. I have yet to use one. I plan to try the ones I mentioned next year. That said, NIST gave astree a good review in 2020: