linux-sparse.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Christopher Li <sparse@chrisli.org>
To: linux-sparse@vger.kernel.org
Cc: Linus Torvalds <torvalds@osdl.org>,
	Josh Triplett <josh@freedesktop.org>,
	Dan Carpenter <error27@gmail.com>
Subject: [RFC] More checking with sparse 0/4
Date: Thu, 28 Dec 2006 01:23:59 -0800	[thread overview]
Message-ID: <20061228092359.GA6573@chrisli.org> (raw)

Hi,

I have been play with sparse to add more Stanford checker style
of checking. The paper is "Checking System Rules Using System-
Specific, Programmer-Written Compiler Extensions" by Dawson Engler
etc.

Unlike the Stanford checker and smatch, this checker is working on
the linearization level instead of AST level. Linearization code
can be very convenient (when it works) to trace the data flow because
pseudo is in SSA form. There is define/user chain to avoid scan
every instruction.

I write the demo of checking null pointer and irq checking. It is mostly
an example.

The checking seems very fast. It adds about 10 seconds to the whole
make C=1 run. We might able to add it to stander sparse checking.

The some of the patch I send it to the list before. I post it again
to make it easy for the people who want to try it out.

As always, comments and suggestions are welcome.

Chris

                 reply	other threads:[~2006-12-28  9:42 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20061228092359.GA6573@chrisli.org \
    --to=sparse@chrisli.org \
    --cc=error27@gmail.com \
    --cc=josh@freedesktop.org \
    --cc=linux-sparse@vger.kernel.org \
    --cc=torvalds@osdl.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).