I write safety critical code, so I've worked with many of these: frama-C, TIS, Polyspace, KLEE, CBMC, and some that aren't on the list like RV-match, axivion, and sonarqube.
With virtually any tool in this category, you need to spend a good amount of time ensuring it's integrated properly at the center of your workflows. They all have serious caveats and usually false positives that need to be addressed before you develop warning blindness.
You also need to be extremely careful about what guarantees they're actually giving you and read any associated formal methods documentation very carefully. Even a tool that formally proves the absence of certain classes of errors only does so under certain preconditions, which may not encompass everything you're supporting. I once found a theoretical issue in a project that had a nice formal proof because the semantics of some of the tooling implicitly assumed C99, so certain conforming (but stupid) C89 implementations could violate the guarantees.
But some notes:
Frama-C is a nice design, but installing it is a pain, ACSL is badly documented/hard to learn, and you really want the proprietary stuff for anything nontrivial.
TrustInSoft (TIS) has nice enterprise tooling, but their "open source" stuff isn't worth bothering with. Also, they make it impossible to introduce to a company without going through the enterprise sales funnel, so I've never successfully gotten it introduced because they suck at enterprise sales compared to e.g. Mathworks.
RV-match (https://runtimeverification.com/match) is what I've adopted for my open source code that needs tooling beyond sanitizers because it's nice to work with and has reasonable detection rates without too many false positives.
Polyspace, sonarqube, axivion, compiler warnings, etc are all pretty subpar tools in my experience. I've never seen them work well in this space. They're usually either not detecting anything useful or falsely erroring on obviously harmless constructs, often both.
With virtually any tool in this category, you need to spend a good amount of time ensuring it's integrated properly at the center of your workflows. They all have serious caveats and usually false positives that need to be addressed before you develop warning blindness.
You also need to be extremely careful about what guarantees they're actually giving you and read any associated formal methods documentation very carefully. Even a tool that formally proves the absence of certain classes of errors only does so under certain preconditions, which may not encompass everything you're supporting. I once found a theoretical issue in a project that had a nice formal proof because the semantics of some of the tooling implicitly assumed C99, so certain conforming (but stupid) C89 implementations could violate the guarantees.
But some notes:
Frama-C is a nice design, but installing it is a pain, ACSL is badly documented/hard to learn, and you really want the proprietary stuff for anything nontrivial.
TrustInSoft (TIS) has nice enterprise tooling, but their "open source" stuff isn't worth bothering with. Also, they make it impossible to introduce to a company without going through the enterprise sales funnel, so I've never successfully gotten it introduced because they suck at enterprise sales compared to e.g. Mathworks.
RV-match (https://runtimeverification.com/match) is what I've adopted for my open source code that needs tooling beyond sanitizers because it's nice to work with and has reasonable detection rates without too many false positives.
Polyspace, sonarqube, axivion, compiler warnings, etc are all pretty subpar tools in my experience. I've never seen them work well in this space. They're usually either not detecting anything useful or falsely erroring on obviously harmless constructs, often both.