On the free side, you also have Frama-C (https://www.frama-c.com) and its Eva plug-in, based on abstract interpretation, and Mopsa (https://mopsa.lip6.fr), also based on abstract interpretation.