Re: Dangerous strcpy
"Vladimir G. Ivanovic" <vgivanovic(a)comcast.net> wrote:
What checkers have you used?
Here are the checkers I've tried out in my 2.5 weeks at the JPL:
Uno: http://spinroot.com/uno/
sparse: http://freshmeat.net/projects/sparse/
CIL: http://cil.sourceforge.net/
splint: http://www.splint.org/
FlawFinder: http://www.dwheeler.com/flawfinder/
Real Soon Now I am going to try:
ITS4: http://www.cigital.com/its4/
MOPS: http://www.cs.berkeley.edu/~daw/mops/
There are lots more to try, of course. Some of the ones listed above
(like splint) are completely ineffective on the XEmacs sources for one
reason or another. (Splint produces too much output when used with
unannotated source code; writing the annotations for that much code
would be a major project.)
The JPL has licenses for some commercial checkers, such as the coverity
and klockwork tools, but I'm not sure if I can legitimately use those on
XEmacs, since it isn't directly related to JPL business. I'll have to
ask. Or maybe we could get the coverity people to donate a code scan,
since the US Department of Homeland Security is paying them to improve
the state of open source software.
I noticed that in a recent Scientific American, there was discussion
of
a number of model checkers. Have you applied any of them to XEmacs?
No, I have not. Model checkers can be very effective at finding design
flaws, but you have to build the model first. There are some tools now
for extracting models from source code, but I have not tried any of them
yet. Note that MOPS, which I mentioned above, uses a model checking
approach.
P.S. When I ran 'make check' I got some errors. I haven't
checked to see
if they've been reported.
There are some known failures. See if the output says "KNOWN BUG"; if
not, please tell us about the failures.
--
Jerry James, Assistant Professor james(a)xemacs.org
Computer Science Department http://www.cs.usu.edu/~jerry/
Utah State University