The best way to use analysis tools is to code in a way that makes it easier for them. Old Orange Book B3/A1 systems had to be coded in a very layered, modular, and internally simple way to facilitate security analysis. Likewise, many of the analysis tools will get lost once you start coding a certain way. Each one also has its strengths and weaknesses.

So, my normal recommendation for people that can't waste time is to use those with few to no false positives combined with a coding style making it easy. For instance, I coded in a structured programming style with relatively simple control flow, quite functional in each unit's structure (see Cleanroom methodology), and avoided hard to analyze things. That made it easy for the tools.

The cool thing is that tools such as Astree and SPARK can prove portions of your code immune to certain defects. Others can do this for concurrency problems. And plain old reviews of design, code, and configuration with a list of common issues can help a lot by itself. That each of these methods has positive results for teams that use them speaks for itself. Them together can be quite powerful.