[bjornsing]

How is it supposed to do that (in the general case)? If I write a C++ program that will index out of bounds iif the Riemann hypothesis is true, then frama-c would have to win the millennium prize to do its job. I bet it can’t.

[bluGill]

Often when I look into questions like this I discover the general case is impossible, but simple hysterics can get 99.999% of the cases and so I can get almost all the benefit even though some rare cases are missed.

[zozbot234]

My own semi-random guess is that "simple hysterics" is indeed how a vast majority (if perhaps not quite 99.999%) of C/C++ devs approaches the code correctness problem - which is why safety mechanisms like the one proposed by OP may in fact be urgently needed. Simple heuristics are likely to be significantly more worthwhile, if appropriately chosen.

[bluGill]

C++ for sure needs better safety mechanisms. And I don't know the exact number of issues simple heuristics can catch.