Static Analysis Tools for C
github.com
github.com
see https://github.com/analysis-tools-dev/static-analysis#multip...
Both repos link each other close to the tops of their respective readmes. Annoyingly, though, the webstite seems to only include the static tools.
valgrind mainly finds memory leaks, buffer overflows and use of unintialized memory. It even works relatively well with some non-C languages.
Example: https://gitlab.com/nbdkit/nbdkit/-/blob/9f96d53dbbbf67ae5ed0...
Valgrind, on the other hand, cares purely about the machine code (with a few exceptions like malloc, free, etc.). It can peek into your libraries even if they aren't compiled with sanitizer flags. It is especially good for finding uninitialized memory usage - IIRC it can track this data even on the level of individual bits in a register.
That's roughly what I do for certain non-embedded work with high performance needs. There's a lot of contract checking and assertions that are too heavyweight for production, so they aren't included in deployment builds. But I certainly wouldn't want to not test at all just because I can't test in production.
Bigger issue for me is what to do when a run time check fails. Sometimes there is nothing to be done but to log the error and reset. Other times, you log the error, clean up and keep going. Which why I dislike rust's run time checks which panic without letting the program try to recover.
Static analyzers are for when your test suite is subpar.
If you're obsessive, like the SQLite guys [1], runtime checkers are better.
But you have to be obsessive about an excessive test suite.
What I said is that runtime checking is better if you have a test suite that's good enough.
A way of discussing it that doesn't place them in competition with each other would instead talk about their relative characteristics, including factors that might make different options more or less effective (or even inapplicable) in certain circumstances.
For example, there are certain classes of defect that cannot be detected at runtime. But what does and does not fall into this category depends on what programming language you're using. There are other classes of defect that cannot be detected statically, and the specifics of this list also depends on what language you're using.
And then there's also a bunch of overlap, but the relative merits of one or another way of solving things cannot be boiled down to a simple "better/worse" hierarchy. The optimal strategy is often domain-specific and finding it may require weighing many tradeoffs.
Absolutely not. It says that they have tradeoffs, and one will be better in certain situations, while the other will be better in others.
If you think that means competition, you're overreading it.
You want a test suite, but it's never better or good enough.
Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
That is a wild claim.
But how many false positives does it have?
Too bad it's not FOSS; I would pay for that is the false positive rate was not too high.
We are talking code without dynamic memory allocation, recursive function calls, no system and library calls, of course. Like some embedded aerospace, automation, healthcare and military applications. You can use it to verify some libraries if you can't do full coverage. Application domain abstractions are also available.
NASA has open source tool called IKOS based on same abstract interpretation concept, but I don't know it's features.
You can't replace testing with formal methods, but formal methods are more powerful when they work. That sqlite hasn't found them useful is just a reflection of how absurdly far out they are on the testing spectrum and how complicated the problem domain they're operating in is (very).
They can demonstrate the bugs, when found, are in the specifications
Or in the methods....
But you're also weakening your own point; you admit that if you test enough, they don't work as well, and you also admit that they work less well the more complicated things get.
The other problem is showing that the artifact you proved is the same artifact that you are using. The enormous amount of effort put in by the seL4 people is proof that that is non-trivial, and seL4 is tiny compared to SQLite.
So when you say, "formal methods are more powerful when they work," you are right, but "when they work" is carrying a lot of weight.
It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker.
Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough.
I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't.
I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.
Sure, if you can. And I use such checkers too.
But for a lot of people, the false positive false negative rates are still high.
That's why tests can be better: there's no false positive or false negative.
> The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't.
This is unfortunately completely naive. Of course model checkers miss things.
Perhaps you're thinking of a static analyzer which is something different.
The ENTIRE POINT of a model checker is that it translates the program into a constraint solver. Can it miss things? Yes, if there is a bug in the translation. It can't be trusted for things that it can't detect, but a model check is equivalent to a constructive proof. It just doesn't have some tools like induction that make constructive proofs necessary in cases where model checking fails.
There is no such thing as a magic tool. The scenarios under model check must be properly built, just like any formal proof. But, a constructive proof assistant and a SMT solver are both forms of proof engines. A model checker uses an SMT solver.
The seL4 team uses model checking as well, in the generated code. They trust model checking in these cases because it's thorough. If it missed things, it would be pointless to use.
So you're saying humans are bad at writing software, but good at writing translations for model checkers?
I disagree.
The reason model checkers miss things is because of humans.
> The seL4 team uses model checking as well, in the generated code.
I am aware, trust me.
Are you aware how much effort they had to expend to do that?
Nice strawman. However, that's not at all what I said. To restate in different words, even proofs can be incorrect. Even model checkers can be wrong. However, you seem to be under the impression that unless a model checker is 100% perfect, it's worthless. That's not the case. For the vast majority of situations, the model checker will either correctly generate a constraint problem based on what you provide (remember, garbage in / garbage out and proofs of bad theorems are meaningless), or will generate some kind of diagnostic error.
Everything -- EVERYTHING -- is flawed. But, if your standard of measure is "only perfect things can augment or replace unit tests" then you're doing yourself and any organization you contribute to a great disservice.
> I am aware, trust me.
Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems.
> Are you aware how much effort they had to expend to do that?
Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort.
Unfortunately, unless you're careful, or have a test suite to make sure, it is the case.
You might have a good model, but if your software doesn't actually implement the model, it's giving you a false sense of security. And those bugs can persist.
> Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems.
Not at all. I know the differences.
But in this context, they all have the same problem: making sure the code matches the model/proof (static analyzers have an implicit internal model).
> Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort.
Ten years of work for four people, I think. That's not 30% overhead. I think at last count, their C code was less than 10 KLoC, but their proof was beyond 200-300 KLoC.
That's a 2000% overhead.
Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect.
Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors.
A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests.
> You might have a good model, but if your software doesn't actually implement the model...
Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP.
> Not at all. I know the differences.
Clearly not, and here's why:
> Ten years of work for four people, I think... That's a 2000% overhead.
The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation.
When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%.
Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.
And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that.
But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.
Highly recommended if you want to get more bang per line of testing code.
In fact, in my current project, I add every single path found by AFL++ to my test suite. It tests all kinds of terrible things, and then those paths are tested forever.
I even run all the paths AFL++ finds through the sanitizers and Valgrind.
No, this statement is quite wrong and expresses a failure to understand the roles and responsibilities of each class of automated tests, and the purpose of static code analysis tools.
Automated tests and static code analysis tools are complementary tools. They don't share responsibilities at all. Just because both can run in the same pipeline stage that does not mean they serve the same purpose.
But I also didn't define "subpar" for a test suite; the SQLite guys have full-coverage testing. That's probably the line for "subpar," and (almost) nobody else actually has that.
No, not really. If you read up on the basics of automated testing, you'll find out that test classes such as unit, integration, UI, performance, accessibility, and localization tests share the same goal: specify and check invariants in the code and in its interfaces.
Static code analysis tools have an entirely different set of responsibilities. They do not have the responsibility of checking the compliance with contracts, including things like SLAs or whether a button is navigatable with a keyboard as per the wishes of a Program Manager.
So what are those responsibilities?
https://en.wikipedia.org/wiki/Static_program_analysis
If you're interested in onboarding onto the topic, you can start by reading the first paragraph of the Rationale section.
> The uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the lint tool) to formal methods that mathematically prove properties about a given program (e.g., its behaviour matches that of its specification).
Sounds like finding defects to me.
You see, I don't think you are. If you were, you certainly wouldn't make totally oblivious claims such as "static analyzers are for when your test suite is subpar."
> Sounds like finding defects to me.
If you were familiar with static analysis tools, you'd be well aware that they only cover a narrow class of defects, which other classes of automated tests do.
Again, I seriously recommend you onboard onto the basics of automated testing, specially the intro section on the classes of tests and what are their design goals, and in the meantime refrain from posting comments on testing.
I only enjoy alphabetical lists of tools, ideally contained in orphaned repositories which have a bunch of outstanding pull-requests, and which are secretly designed to lure clicks to their sponsors if they've got red-heart emojis and reference the price of a cup of coffee.
AI overlords never drink coffee, so they can't appreciate what it means to sponsor such lists.
* https://github.com/dense-analysis/ale/blob/master/supported-...
While less comprehensive¹, this is my go-to list when I start working with a new language. Just brew/yum/apt installing the tool makes it work in the editor²
¹this list mostly has foss,static analyzers, however anyone can contribute (mine was the gawk linting)
²alright, there are some tools that might need some setup
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.
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?
See every embedded dev tool
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
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 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 =)
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.
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.
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...
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.
And to rub salt into the wound, the Annex K functions supplied with MSVC are non-conforming to the standards Annex K functions, which were also pushed hard by Microsoft, which make them kinda doubly pointless: you use them and make code that is neither portable to another compiler nor conforming to the standard :-/
As more tools move to a subscription based model, I don't want to tie myself down to 5 subscriptions just to maintain some ancient code.
Of course if you are content to sit back several versions (without support) the above doesn't make sense. As you say, if the code itself you are looking at is ancient and only minimally maintain it isn't worth keeping subscriptions and it would be better to have a permanent license to tools that you won't change.
Especially when you're developing software for safety applications, it becomes important to maintain/archive the same tools/compilers/libraries so that rebuilding old code in a few years still produces the exact same binary.
So at that point it's not as important to have the newest and shiniest tools, but more important to pay for a tool once and know that it works reliably.
This site is making money from open source free tools, (where the site claims it's open source) asking for contributors to contribute for free and not giving back to them or the authors of the tools.
We have no clue about where the money is going as this site isn't transparent even though they claim they are 'open source'
Is the sponsor money also going to these open source projects as well and what is the proportion?
for c++ I use clang-tiday and cppcheck, neither can handle all c++20 though with noisy false positives, but better than not using them
Ultimately, this is a nitpick on the website. However, the whole point of static analysis is that you're nitpicking because not nitpicking can sometimes have disproportionate consequences. So I agree that it would be nice if they cleaned up that particular section to be a bit more accurate.
I know this is sarcasm, but there's a reason Greenspun's tenth rule holds true.