For C, Frama-C + Eva plug-in does essentially the same job as Astrée (with small differences of support for specific features) and is open-source and freely ava

For C, Frama-C + Eva plug-in does essentially the same job as Astrée (with small differences of support for specific features) and is open-source and freely available. (There is an experimental C++ front-end, but it is not ready for industrial size C++ that makes extensive use of the standard library)