smatch warnings in current upstream kernel

Here are the 7161 smatch warnings for 2139 files in upstream head 1a95620f45155ac523cd1419d89150fbb4eb858b. It's not a complete build (no make clean), so does not include all possible warnings.

Quoted 4 lines · Fengguang Wu

Here are the 7161 smatch warnings for 2139 files in upstream head 1a95620f45155ac523cd1419d89150fbb4eb858b. It's not a complete build (no make clean), so does not include all possible warnings.

There are some sparse warnings mixed in as well. They would have been sent to stderr and smatch warnings get sent to stdout.

But if you want you could look at smatch_scripts/test_kernel.sh which allows for a parallel build and saves all the warnings in warns.txt.

I guess you have your own parallel build technique as well and that works too.

On Tue, Sep 11, 2012 at 01:51:27PM +0300, Dan Carpenter wrote:

$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

Quoted 3 lines · Fengguang Wu

On Tue, Sep 11, 2012 at 01:51:27PM +0300, Dan Carpenter wrote:

$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

Some of the warnings you are getting seem to mean that you're not picking up the smatch_data/ directory. For example some of the buffer overflow errors:

drivers/mtd/ubi/wl.c:336 prot_queue_add() warn: buffer overflow 'ubi->pq' 10 <= 10

What is happening in that function is that Smatch sees the:

	ubi_assert(pq_tail >= 0 && pq_tail < UBI_PROT_QUEUE_LEN);

and assumes that since there is a test for
"pq_tail < UBI_PROT_QUEUE_LEN" then it must be possible for pq_tail = UBI_PROT_QUEUE_LEN. There is a file called:
smatch_data/kernel.ignored_macros which has ubi_assert() and it means to ignore everything that happens inside a ubi_assert().

Normally Smatch looks for the data dir with the binary, but you can also specify a directory with --data=/path/to/smatch_data/. Then

you can test that it's working by doing a:
kchecker drivers/mtd/ubi/wl.c
to verify that the warning goes away.

Quoted 4 lines · Dan Carpenter

Quoted 3 lines · Fengguang Wu

On Tue, Sep 11, 2012 at 01:51:27PM +0300, Dan Carpenter wrote:

$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

FYI, the wrapper script is as simple as

SMATCH=/c/smatch/smatch
$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

Quoted 6 lines

Some of the warnings you are getting seem to mean that you're not picking up the smatch_data/ directory. For example some of the buffer overflow errors:

drivers/mtd/ubi/wl.c:336 prot_queue_add() warn: buffer overflow 'ubi->pq' 10 <= 10

Quoted 8 lines

What is happening in that function is that Smatch sees the:

	ubi_assert(pq_tail >= 0 && pq_tail < UBI_PROT_QUEUE_LEN);

and assumes that since there is a test for
"pq_tail < UBI_PROT_QUEUE_LEN" then it must be possible for pq_tail = UBI_PROT_QUEUE_LEN. There is a file called:
smatch_data/kernel.ignored_macros which has ubi_assert() and it means to ignore everything that happens inside a ubi_assert().

Yes, I can see the data and function. Thank you very much for the tips!

Quoted 2 lines

Normally Smatch looks for the data dir with the binary, but you can also specify a directory with --data=/path/to/smatch_data/. Then

The directory layout here is

/c/smatch/                      # git tree 
/c/smatch/smatch                # binary
/c/smatch/smatch_data/          # kernel.* data

Quoted 3 lines

you can test that it's working by doing a:
kchecker drivers/mtd/ubi/wl.c
to verify that the warning goes away.

Both of these two tests run well w/o the above warning:

/c/smatch/smatch_scripts/kchecker drivers/mtd/ubi/wl.c

make C=1 CHECK=/c/kernel-tests/smatchcheck drivers/mtd/ubi/wl.o

This is interesting. I'll try adding --data=/c/smatch/smatch_data and check whether the end result becomes better.

Quoted 43 lines · Fengguang Wu

Quoted 4 lines · Dan Carpenter

Quoted 3 lines · Fengguang Wu

On Tue, Sep 11, 2012 at 01:51:27PM +0300, Dan Carpenter wrote:

$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

FYI, the wrapper script is as simple as

SMATCH=/c/smatch/smatch
$SMATCH -p kernel "$@" > $SMATCH_OUT_ROOT/$PPID-$$-$RANDOM

Quoted 6 lines

Some of the warnings you are getting seem to mean that you're not picking up the smatch_data/ directory. For example some of the buffer overflow errors:

drivers/mtd/ubi/wl.c:336 prot_queue_add() warn: buffer overflow 'ubi->pq' 10 <= 10

Quoted 8 lines

What is happening in that function is that Smatch sees the:

	ubi_assert(pq_tail >= 0 && pq_tail < UBI_PROT_QUEUE_LEN);

and assumes that since there is a test for
"pq_tail < UBI_PROT_QUEUE_LEN" then it must be possible for pq_tail = UBI_PROT_QUEUE_LEN. There is a file called:
smatch_data/kernel.ignored_macros which has ubi_assert() and it means to ignore everything that happens inside a ubi_assert().

Yes, I can see the data and function. Thank you very much for the tips!

Quoted 2 lines

Normally Smatch looks for the data dir with the binary, but you can also specify a directory with --data=/path/to/smatch_data/. Then

The directory layout here is

/c/smatch/                      # git tree 
/c/smatch/smatch                # binary
/c/smatch/smatch_data/          # kernel.* data

Quoted 3 lines

you can test that it's working by doing a:
kchecker drivers/mtd/ubi/wl.c
to verify that the warning goes away.

Both of these two tests run well w/o the above warning:

Quoted 6 lines

/c/smatch/smatch_scripts/kchecker drivers/mtd/ubi/wl.c

make C=1 CHECK=/c/kernel-tests/smatchcheck drivers/mtd/ubi/wl.o

This is interesting. I'll try adding --data=/c/smatch/smatch_data and check whether the end result becomes better.

It works now, after changing '-p kernel' to '--project=kernel'.

Next step would be to regenerate the smatch_data/ contents for each new branch to make it work more reliably.