Date: Sun, 27 Jul 2003 11:54:57 +0200 From: Alexander Leidinger <Alexander@Leidinger.net> To: "Poul-Henning Kamp" <phk@phk.freebsd.dk> Cc: cvs-all@freebsd.org Subject: Re: cvs commit: src/sys/kern init_main.c kern_malloc.c md5c.c subr_autoconf.c subr_mbuf.c subr_prf.c tty_subr.c vfs_cluster.c vfs_subr.c Message-ID: <20030727115457.553f1df7.Alexander@Leidinger.net> In-Reply-To: <56900.1059255288@critter.freebsd.dk> References: <20030725212142.GB9176@cirb503493.alcatel.com.au> <56900.1059255288@critter.freebsd.dk>
next in thread | previous in thread | raw e-mail | index | archive | help
On Sat, 26 Jul 2003 23:34:48 +0200 "Poul-Henning Kamp" <phk@phk.freebsd.dk> wrote: > When I first started to interest myself with the mechanics of > sanitizing the kernel source, it was because two common symbols had > the same name, which gave rather non-newtonian behaviour under a > given set of circumstances which I ran into rather often. > > Subsequently, I have written a couple of minor scripts to try to > help make sure certain kinds of consistency remains in force in the > kernel (this was the genesis of src/tools btw). > > I have even gone as far as to spend a fair bit of time testing > various code analysis tools, a decade ago I used Purify, these days > FlexeLint is my favourite, on the kernel correctling as I go the > most severe problems I found that way. [...] > We still have no tools which help us translate high level abstractions > into low level code or for that matter to validate the high level > abstractions in the first place. Are you talking about e.g. model checking? After Aug 2 I plan to look at porting 2 major open source model checkers. > Given all that, I firmly belive we should embrace every little bit > of help we can get from tools and programs we have, even if that > means minor inconveniences and a certain cramping of style here and > there. Perhaps you can convince dds (CCed) to extend devel/cscout in various helpful directions. Based upon his introduction to us at the time he got his commit bit and his homepage he may be interested in this kind of work. Bye, Alexander. -- "One world, one web, one program" -- Microsoft promotional ad "Ein Volk, ein Reich, ein Fuehrer" -- Adolf Hitler http://www.Leidinger.net Alexander @ Leidinger.net GPG fingerprint = C518 BC70 E67F 143F BE91 3365 79E2 9C60 B006 3FE7
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20030727115457.553f1df7.Alexander>