On 24 Oct 2009, sch...@yahoo.com wrote: --- On Sat, 10/24/09, David Evans <ev...@cs.virginia.edu> wrote:
>> A better design would just use the parser as a front end to produce >> an intermediate representation which would be used for all the >> analysis, but the actually implementation intertwines the parsing >> and analysis much more than it should. For an IR, are you saying something like GENERIC? > Is this the approach being taken by ggcc? > http://ggcc.info/ > Perhaps an splint plugin to their frame work would be the way to go? Looking, this seems to be a global static analysis attempt. This is similar to Coverity Prevent, Polyspace verifier, etc. These use global analysis to determine thing that splint would determine through annotations. As the program determines them, there is no need to annotate, but they take significantly longer to run. I think these are significantly different? GCC has a plug-in framework in 4.5 and better. http://gcc.gnu.org/onlinedocs/gccint/Plugins.html http://gcc.gnu.org/wiki/plugins-branch However, comments (and hence splint annotations) would be discarded by the lexer. I don't believe that a plugin would have access to these (?). An alternative is to use the 'attribute' syntax to describe preconditions, postconditions and other criteria. I think that a splint plug-in for gcc would be more likely, but I am not so sure that it can't be a stand-alone program. fwiw, Bill Pringlemeir. -- I find this continuous feedback and interplay between pure mathematics and theoretical physics most fascinating. - Marco _______________________________________________ splint-discuss mailing list splint-discuss@mail.cs.virginia.edu http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
