Smatch: pluggable static analysis for C

Posted Jun 23, 2016 21:41 UTC (Thu) by mstefani (guest, #31644)
Parent article: Smatch: pluggable static analysis for C

I am not sure that the "wine" project in Smatch works. I have been using the old gcc based Smatch successfully on Wine and Dan has been very kind to port some of the stuff I used over to the new Smatch. But for Wine the new Smatch suffered from two big problems:
- Sparse couldn't compile Wine.
- I'm not a compiler or even CS guy and sparse and the new Smatch were too steep for me to learn and fix.

So I kept using the old Smatch for as long as it still run and was able to compile Wine. By that time coccinelle came along and I started using that. Coccinelle had the advantage of being useful also for my other Wine work aka massive automated code changes.
Though not everything can be done with coccinelle and I always planned to go back and look at Smatch. Thanks for the article.

Smatch: pluggable static analysis for C

Posted Jul 1, 2016 14:25 UTC (Fri) by error27 (subscriber, #8346) [Link]

I hadn't testing wine for some time.

I have pushed an update so you don't need to do Neil's -I/usr/include/x86_64-linux-gnu/ work around that he mentions in the other comment. Also I changed it to ignore _Pragma() instead of dying. There are still one or two files that don't compile because they use the tools/winegcc/winegcc wrapper instead of regular gcc and I didn't investigate how to deal with that.

The main thing though was that it wasn't ignoring the ok() macro and the list of no return functions was out of date. I also updated the smatch_scripts/ directory to take a -p=<project> argument. The thing which I haven't managed to do yet is to make the cross function db work properly.

CHECK="~/progs/smatch/devel/smatch --file-output --full-path -p=wine" \
make CC="~/progs/smatch/devel/cgcc"
find -name \*.c.smatch -exec cat \{\} \; > smatch_warns.txt

You could pass a -j8 or whatever to the make to speed things up.

The warnings are still pretty low quality compared to the kernel because I've massaged Smatch for the kernel's quirks. :/ The kernel has a pretty uniform style so there are some issues I never noticed until now.