I find it depends a lot on the static analyzer. (My experience is largely with C code.) In particular, if the analyzer produces a lot of false positives it is dumping a pile of work onto the developers to work through each report and satisfy themselves that it's invalid, and hiding the real bugs under a pile of garbage. If it is more careful to avoid false positives then it's more workable as a development tool (but of course it then finds fewer interesting issues).

The other key static analyzer question is "how easy is it to run and does that happen early in the development cycle?". A static analysis pass built right into the compiler and generating warnings every time you compile has the most chance of having its reports paid attention to. Something that runs at CI time is more annoying. Something that runs only on trunk a week or more behind the leading edge of development and which just lists its reported issues on a webpage somewhere is in grave danger of being outright ignored, or only read by one or two enthusiasts who are forever fixing up other peoples' code...

I lead a Go team, and we pretty much never go (heh) anywhere without a suite of static analysers. go vet, govulncheck, errcheck, and staticcheck are the required minimum, but we do use some others.

Back when I used to write Ruby, lack of static analysis was a serious problem. I've been able to add Rubocop later, but it's not exactly on the same level as staticcheck, to say nothing about Prusti from the OP.

Could you comment on the others you use? I would like to start using a lot more static analysis at $job.

Luckily for you, it's all open-source, heh.

https://github.com/AdguardTeam/AdGuardDNS/blob/master/script...

https://github.com/AdguardTeam/AdGuardDNS/blob/master/script...

There's some mess in there, but if you only need a list of analysers and examples of usage, these should be enough.

Big tech uses static analyzers a lot. See for example, these projects:

- https://fbinfer.com/ (<- This one was a breakthrough in static analysis in its time)

- https://github.com/google/error-prone

- https://github.com/facebook/SPARTA

And many others

Many of Google's general checks in clang-tidy should be directly available, too. For example, the absl checks seem to be on the list of clang-tidy checks:

https://clang.llvm.org/extra/clang-tidy/checks/list.html

Microsoft bought and adapted PREfix and created a simpler, faster version called PREfast (and the Visual Studio -analyzer switch for C/C++/C# code).

see tools section in https://learn.microsoft.com/en-us/previous-versions/tn-archi...

When I worked on a big c++ codebase I found them essential for both ci/cd systems and actively debugging an issue. The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind if you're writing c/c++ code for a platform valgrind runs on.

On the other hand commercial tools have been more of a mixed blessing but that is probably because every time ive seen them deployed the budget hasnt included sufficient engineering time, training or prof services to cut down huge numbers of false positives.

> The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind

valgrind is not a static analysis tool. But it is a great tool, especially memcheck.

They work really well, and people, while initially skeptical, eventually get the idea. The key is to run a first pass on your codebase, find and fix real bugs, and share your findings. This turns a very theoretical tool into 'see, it works, and that's one nasty bug we won't have in production'.

I'm a "hard core PLer" and I am skeptical. I don't like automated solvers where there is no way to manually include a proof (to be checked).

In the typical enterprise projects I work on they are quite typical, usually we tend to use stuff like SonarQube and it breaks the build for specific errors.

Usually it doesn't matter if devs themselves don't care, because when devops have the management support, they will care to fix that broken build.

A lot of Python teams use a linter that can catch errors like "variable used before defined" as well as matters of code style, and increasingly a static type checker in addition to that (which also does its own set of such checks).

Static analyzers are free CR in most cases. I highly recommend using it, and do know that in some companies people are unaware of those unfortunately..

I can't even convince my co-workers to use Typescript. :-/

I think it varies by industry though.

We have some critical systems code in C that I'm going to try to run static analysis on for our Hack Week. There are probably 100 engineers at my company and not much interest in anything beyond Google SRE and language specific release updates. We use Bash, Php, Python, Ruby, Node, C, Go, and Rust.

Not sure how relevant my experience is, but I work on a 30+ year old Windows application that started life as a DOS application. It is written in a mix of C and C++. We still do things pretty old school. As part of submitting your work for code review (which is required for every change), you submit the output of cppcheck. When we first introduced cppcheck, there were thousands of warnings and errors that we slowly worked through. Now it is expected that the cppcheck output is empty.

That's what scares a lot of people when they run a static analyzer on code for the first time - all the possible problems.

Some of the possible problems are easy to confirm or deny just by looking at one line of code, but others will require much more analysis.

You need a tool/viewer to show the possible problem and what caused the possible problem. Such a tool improves the user experience dealing with static analyzer results.

Our CI test run includes mypy; even in the mode where it skips certain checks, it finds subtle, non-obvious bugs time and again.

I run mypy as a part of Emacs flycheck mode for Python.

Switching on a static analyzer is usually somehow painful, because old code does not typecheck, or has issues that static analysis discovers but which never get triggered in real life. You have to face constant (and rightful) nagging until you fix all key parts of your code so that the static analyzer no longer has concerns.

In his regard, Python is noticeably behind Typescript, because TS's type system and other amenities allow for more complete and precise descriptions of invariants that hold in the program, and which static analysis tools check.