3 ms·
sparse -- adds annotations to kernel code which can be checked by the compiler. It is a little bit like a parallel type system which provides domain-specific k
by colin_mccabe 11y ago
sparse -- adds annotations to kernel code which can be checked by the compiler. It is a little bit like a parallel type system which provides domain-specific knowledge like "this function takes lock A and then lock B" or "this function runs in interrupt context." See https://sparse.wiki.kernel.org/index.php/Main_Page https://sparse.wiki.kernel.org/index.php/Main_Page
kmemcheck -- sort of like valgrind, but for the kernel.
CONFIG_FAULT_INJECTION -- inject random faults at runtime (such as in memory allocation) to test infrequently encountered error paths.
CONFIG_DEBUG_MUTEXES, CONFIG_DEBUG_SPINLOCK -- run expensive mutex validation checks at runtime.
coccinelle -- a source code matching and transformation engine. You can use it in some of the same contexts as sed or awk. Unlike those tools, it is aware of the C language so it can do smarter things like add an extra final argument to all occurrences of a call to do_foo_bar_baz(). See http://coccinelle.lip6.fr/ http://coccinelle.lip6.fr/
checkpatch.pl -- Checks a patch to see if it conforms to the kernel style guide. Simple things like enforcing 80-column lines, but also more complicated things as well like variable naming, whitespace, etc.
smatch, flawfinder -- static analysis tools that are similar in principle to Coverity. Like Coverity, they are unsound, but often helpful.
- xjia 11y agoThanks for the summary. However, what do we have on the formal proof side?