4 ms·
What are those tools?
by xjia 11y ago
What are those tools?
- colin_mccabe 11y agosparse -- 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?