[emillon]

It's impossible to have a static decision procedure about dynamic properties of programs, such as the size of dynamically allocated memory areas (Rice's theorem). So, it is necessary to either include false positives (correct programs rejected) or false negatives (incorrect programs accepted).

Sound static analyzers fall in the first case, but require a lot of work to become precise enough to be used (ie, to reduce the number of false alarms). Compilers fall in the second case in the sense that they don't have to honor such a clause. And in the C99 norm it's actually a "shall" (it just couldn't honor a "must" in that case):

"If the keyword static also appears within the [ and ] of the array type derivation, then for each call to the function, the value of the corresponding actual argument shall provide access to the first element of an array with at least as many elements as specified by the size expression."

[eru]

> It's impossible to have a static decision procedure about dynamic properties of programs, such as the size of dynamically allocated memory areas (Rice's theorem).

You can not have a general procedure, but with the help of the programmer / user of the compiler, you can prove all kinds of things.