| |||||||||||||
|
| |||||||||||||
SPLINTSPLINTPosted Jun 10, 2009 1:17 UTC (Wed) by vonbrand (subscriber, #4458)In reply to: SPARK is MetaL for Ada? Tokeneer is a program written in SPARK? by AnswerGuy Parent article: SPARK toolsuite released under the GPL
This sounds awfully similar to splint. I tried (a bit) writing programs that pass its checks, and gave up (I could find no way to write linked list manipulation). Not that I tried too hard. David A. Wheeler has a (dated) page on packages for checking source code for problems. The basic problem is that proving anything is hard work. And as long as very few people use it, and even less are competent to hack on it, much of the advantage of open source becomes moot. Sadly.
(Log in to post comments)
splint --- secure programmer's 'lint' Posted Jun 10, 2009 8:12 UTC (Wed) by AnswerGuy (guest, #1256) [Link]
I know about splint and Linus' "sparse." I neglected to mention them in my comment for a couple reasons.
splint, like RATS, is focused on parsing and scanning sources for security vulnerabilities ... and adding "magic comment" (annotations) support is somewhat optional for them. It helps them find some vulnerabilities that couldn't be statically detected without a bit of extra help.
sparse has an unfortunate name. Horrifically unfriendly in a search engine world. There's also no online documentation for it that I can find. We learn from very short blurbs that it's a source code parser but we get know sense of how advanced it may have become and whether it's actively maintained, etc. I see that it was a candidate for Google SOC (summer of code) sponsorship. But I don't see that anyone signed up for project to work on sparse.
I haven't used any of these tools. I'm primarily a sysadmin and trainer (on sysadmin focused topics). The "programming" that I do is mostly in Python or Perl ... or Bourne shell ... and thus is relatively lightweight.
I would, however, love to see some in-depth discussion of some of these tools ... with practical HOWTO and case study stories. (Perhaps a tale of how a qualified developer took $TOOL ... applied it to $PROJECT_CODE and discovered $VULNERABILITIES by running the tool and refining annotations to it.
Perhaps Jon and his associates will host a series of articles by people who are far more qualified that I am on this sort of topic. (I wonder if Valerie Aurora or Ulrich Drepper would be so inclined.
sparse: not a search-unfriendly name Posted Jun 10, 2009 15:57 UTC (Wed) by JoeBuck (subscriber, #2330) [Link] You write that "sparse" has a poorly-chosen name in a search-engine world, but you clearly didn't search for it. Google's top choice for "sparse" is, in fact, Linus's Sparse tool.If you think about it, the reason is clear: "sparse" is an adjective, and people searching for, say, sparsely populated areas or sparse matrix libraries would have to include at least two words. A one-word search has to refer to some product or program named "sparse".
sparse: not a search-unfriendly name Posted Jun 10, 2009 17:11 UTC (Wed) by ballombe (subscriber, #9523) [Link]
> You write that "sparse" has a poorly-chosen name in a search-engine world, but you clearly didn't search for it.
How is it clear ? One find only one relevant link (to http://www.kernel.org/pub/software/devel/sparse/) whose content was summarized by the grand-parent post, and does not include documentation.
sparse: not a search-unfriendly name Posted Jun 11, 2009 20:46 UTC (Thu) by nix (subscriber, #2304) [Link]
Does it make me an idiot that I only just figured out that the name is
split 's-parse', i.e. 'source parse'? I've been wondering why it was called that and what it had to do with sparseness for some years now...
SPLINT Posted Jun 10, 2009 22:31 UTC (Wed) by Wol (guest, #4433) [Link]
If problem 1 is that proving anything is hard, problem 2 is that Godel says the proof is meaningless.
While the incompleteness theorem doesn't say this exactly, when applied to computer proofs you end up with one of three conclusions:
1 - the problem is so simple why are you using a computer?
Okay, doing a formal proof is often worth it for finding bugs, but if the client wants confirmation that the program actually works then a mathematical proof (ANY proof) is worthless.
Cheers,
value of proving properties of software Posted Jun 11, 2009 12:20 UTC (Thu) by pjm (subscriber, #2080) [Link] Regarding conclusion 1, there are lots of properties that don't require great intellect to prove, but do require lots of mechanical operations that computers are good at and that humans make errors with. Proving that array accesses are in bounds, or that a heap invariant is always maintained, is a valuable service that a compiler or other static checker can provide. As Wol points out, automated checks (or occasionally even constructing a formal proof semi-manually) are often worth it for finding bugs (or for directing one's effort when searching for cause of a bug). For me, this means that the proof isn't meaningless. (Incidentally I don't see the connection between Gödel's incompleteness theorems and either the claim that the proof is meaningless or the claim that those three conclusions are the only possibilities.)
|
|
||||||||||||