It's true claim, no potential error is ever omitted. It may be hard to get code pass because there are false alarms, but when it passes it holds. We are talki

It's true claim, no potential error is ever omitted. It may be hard to get code pass because there are false alarms, but when it passes it holds. We are talking code without dynamic memory allocation, recursive function calls, no system and library calls, of course. Like some embedded aerospace, automation, healthcare and military applications. You can use it to verify some libraries if you can't do full coverage. Application domain abstractions are also available. NASA has open source tool called IKOS based on same abstract interpretation concept, but I don't know it's features.