Static Analysis tool for Linux kernel modules and device drivers

Question

I need a static analysis tool for the Linux Device Drivers I write for ARM based boards. I am considering few tools as mentioned below:

1. Sparse is a computer software tool, already available on Linux, designed to find possible coding faults in the Linux kernel.

2. There are two active projects of Linux Verification Center aimed to improve quality of the loadable kernel modules.

   • Linux Driver Verification (LDV) - a comprehensive toolset for static source code verification of Linux device drivers.
   • KEDR Framework - an extensible framework for dynamic analysis and verification of kernel modules.
   • Another ongoing project is Linux File System Verification that aims to develop a dedicated toolset for verification of Linux file system implementations.
3. Enable -Werror, -Wextra and -Wall on GCC, and run with Valgrind.

Last time I played with Sparse I found the outputs to be confusing and did not find a good documentation to interpret the output. Does anyone has a good documentation on Sparse tool? What are the other Free static analysis tools I can use for my Linux driver verification? I know about LINT tool but its licensed.

Answer 1

Smatch is a static analysis tool for C that is used on the kernel. It has resulted in hundreds of patches. Quite a few have been security related or were significant enough for the stable kernel.

Answer 2

If you want to write your own rules, Coccinelle is probably appropriate. If you want to use rules written by others you can use the various tools integrated into the kernel. Check section 4.2: CODE CHECKING TOOLS of Documentation/development-process/4.Coding for some suggestions.