Does anyone use any of these tools as part of their professional life?
I would love to know which tool you use and how it's used.
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.
See every embedded dev tool
That's interesting. What kind of documentation would you expect in addition to ACSL by Example and the WP tutorial?
What are the proprietary components that you miss the most?
Don't forget that real errors you fix will disappear so even a few false positives are bad because you see them all the time and so they seem worse than they are.
Now that our tools have a zero false positive policy we can require all attempts to silence warnings are allowed only after a bug report is opened with the tool. Everytime we upgrade we grep and remove the silence warning comments for things fixed.
The potential for an issue may be legitimate, but that doesn't make it a false positive.
If there is a clear fix that makes the code objectively better then I'm for the tool. However if it warns about correct code because of a potential issue that doesn't even apply that is a false positive.
Periodically, run other static analyzers like Klocwork and Coverity. They can catch many more issues than Clang. It's not that Clang is bad, but it has inherent limitations because it only analyzes a single source file and stops analysis when you call a function from another module
I also do time critical stuff, so llvm is a nonstarter for predictive latency in code motion. For most other use-cases, clang/llvm typically does improve performance a bit, and I do like its behavior on ARM.
Happy coding =)
Nowadays that's only the default. But you can enable "cross translation units" [1] support to perform analysis across all the files of an application. It's easier to deploy CTU by using CodeChecker [2].
Also for the Clang static analyzer: make sure the build does use Z3. It should be the case now in most distro (it's the case in Debian stable ;). It will improve the results.
With both CTU and Z3 I'm very happy with the results. Klocwork mostly only reported false alarms after a clean CodeChecker pass.
[1] https://clang.llvm.org/docs/analyzer/user-docs/CrossTranslationUnit.html
[2] https://codechecker.readthedocs.io/en/latest/I tried to use Frama-C a while back and gave a talk about it, but for us it wasn't too practical: http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4
One should use a fault tolerant design pattern... especially in C. i.e. assume stuff will break, interleave guard variables, and use buffer safe versions of standard string functions. There are also several back-ported data-structure libraries for C that make it less goofy to handle.
Personally I like designing systems like an insect colony, avoid thread safety issues, and constantly life-cycle individual modules. This makes things easy to scale/audit, kinder to peers who read 2 pages to understand the codes purpose, and inherently robust as locality is unnecessary to continue to function (parts can fail back and self-repair while running).
Have fun. =)
This to complement unit and integration tests in simulation, with all sanitizers (UBSAN, ASAN, MSAN, TSAN).
Both are useful. In practice, the runtime tests catch most bugs. But now and then some bug sleeps through and is caught by the Clang static analyzer. It's always impressive to see a display of 30+ steps leading from an initial condition to a bug.
Finding bugs is the the static analyzer really. Clang tidy (a linter) is for code "cleanliness" and avoiding dangerous constructs. But I don't remember tidy finding a real issue, contrary to the static analyzer.
For command line builds I'm planning to migrate to clang-tidy though (contrary to popular belief clang-tidy is not just a linter, it also runs the clang static analyzer checks).
Visual Studio also comes with their own static analyzer, but this doesn't seem to be as thorough as Clang's.
Also: static analyzers are just one aspect, the other is runtime sanitizers (e.g. clang's ASAN, UBSAN and TSAN).
I've used the "professional" security ones including TrustInSoft and Synopsis tools. They are pretty cool, but give a lot of false positives, you either need teams to really understand the security model of these systems, or to have a dedicated team manage and triage things.
They do a great job catching some egregious mistakes though.
That being said, I think Rust is takes the better approach of trying to build safety directly into the language and compiler. Though I think there is still a lot of room for innovation here.
Yeah, this extension is almost the default choice for vscode https://marketplace.visualstudio.com/items?itemName=ms-vscod...
And while clang-tidy is integrated with the MS C++ extension, it needs to be run manually, or automatically on file save/open (see: https://devblogs.microsoft.com/cppblog/visual-studio-code-c-...) - I guess it's too expensive to just run in the background while typing.
https://learn.microsoft.com/en-us/cpp/ide/cpp-linter-overvie...
These are usually linters, not proper static analyzers (although the popular clang-tidy is a bit of both).
A "proper" static analyzer follows control flow and tries to cover all possible variations (and then reporting things like "this pointer here will be null when this other function 10 levels up the callstack is called with parameter "x" having the value "N" - Xcode even gives you a control-flow visualization overlayed as arrows over the source code to give a better idea how the static analyzer arrived at that conclusion).
Running code through a static analyzer takes many times longer than compiling the code.
> They are pretty cool, but give a lot of false positives.
Analyzers usually take assert() as hints (e.g. 'assert(ptr)' hints to the analyzer that ptr isn't expected to be null - so you won't get a "this pointer can potentially be null" false positive. The tighter your assert checks, the fewer false-positives you'll get.
Anything that looks at code without running it qualifies.
I don't know what you mean by "proper" static analyzer. The static analyzer libraries that I use do produce lint, but this is among many other useful insights.
In the old days I used stuff like Insure++.
Additionally when using C is unavoidable, taking a abstract data types design approach[0], to minimize killing data structure invariants as much as possible.
Otherwise, I've used flawfinder for some of my projects.