Smatch: a source code checker

Pedro F. Giffuni giffunip at
Fri Sep 26 17:06:01 PDT 2003


Smatch is a, relatively small, patch to gcc 3.1.1 to do configurable checks on
code (there is a good number of examples scripts on the CVS). It should be easy
to integrate it as an option for our gcc31 port but I got scared when I saw the
complexity our gcc31 port already has ;). Maybe someone more familiar with the
gcc ports finds this interesting.

"Smatch is C source checker but mainly focused checking the Linux kernel code.
It is based on the papers about the Stanford Checker. 

Basically, Smatch uses a modified gcc to generate files. The files
are piped through individual Smatch scripts that print out error messages. 

For example, someone might want to write a Smatch script that looked for code
that called copy_to_user() while the kernel was locked. If the script saw a
place that called lock_kernel() then it would record the state as locked. If
the script saw a place that called unlock_kernel() it would set the state to
unlocked. If the state was locked and the script saw a place that called
copy_to_user() the script would print out an error message. 

The tricky part is when a programmer says something like: "If this that or the
other thing is true then unlock the kernel otherwise don't." After a while* he
might forget whether the kernel is locked or unlocked and call copy_to_user().
Smatch scripts use the library to keep track of what the state is so
sometimes they find mistakes that the programmer might miss. 

There are lots of rules that can be written in Smatch scripts: 

* Don't call copy_to_user() while the kernel is locked 
* If a variable is uninitialized don't use it 
* If a variable is possibly NULL don't use it until you have checked 
* If you free() a variable, don't free() it again 

Since writing Smatch scripts is so easy, coders can check for things specific
to their own programs. One user described writing his script as, "a trivial
task." Some scripts are harder than others, of course. If you have a hard time
writing your script email us at smatch-discuss[at] If it is a
kernel related script, it would be nice to add it to the Smatch CVS. If it is
not kernel related email us anyway."



Do you Yahoo!?
The New Yahoo! Shopping - with improved product search

More information about the freebsd-ports mailing list