Static Analysis: results of FUDcon Lawrence hackfest
Daniel P. Berrange
berrange at redhat.com
Fri Jan 25 13:03:06 UTC 2013
On Fri, Jan 25, 2013 at 12:51:13PM +0000, Richard W.M. Jones wrote:
> On Fri, Jan 25, 2013 at 01:18:43PM +0100, Kamil Dudka wrote:
> > On Friday, January 25, 2013 09:07:22 Richard W.M. Jones wrote:
> > > On Thu, Jan 24, 2013 at 02:11:11PM -0700, Jerry James wrote:
> > > > Note that we also have why and why3 in Fedora, by the way.
> > >
> > > .. and ocaml-cil.
> >
> > CIL can be used as a front-end for a static analysis tool or a C preprocessor
> > for static analysis tools that have limited C language parsing capabilities,
> > but how are you going to use CIL as a static analysis tool on its own?
>
> Well I did try. Not, it has to be said, very successfully:
>
> http://people.redhat.com/~rjones/cil-analysis-of-libvirt/
Based on your work I actually used CIL to validate the correctness of
mutex locking in libvirt with pretty good success
https://www.berrange.com/posts/2009/05/15/static-analysis-to-validate-mutex-locking-in-libvirt-using-ocaml-cil/
the analysis script has bit-rotted since i first wrote it, since
libvirt locking policy has changed, but it should be possible to
bring it up2date. It identified a good set of bugs, which I don't
believe tools like coverity are able todo, because they lack the
semantic knowledge about intended locking behaviour in this area.
> This brings me back to an earlier post I made which I still think has
> an important point to make:
>
> http://lists.fedoraproject.org/pipermail/devel/2012-December/175324.html
Yep, if I ever have some free time, I have long planned to make
use of CIL to validate the virError reporting item you mention
there. It would clear out a large set of bugs that are basically
impossible to validate any other way than by writing a custom
static analysis script.
Daniel
--
|: http://berrange.com -o- http://www.flickr.com/photos/dberrange/ :|
|: http://libvirt.org -o- http://virt-manager.org :|
|: http://autobuild.org -o- http://search.cpan.org/~danberr/ :|
|: http://entangle-photo.org -o- http://live.gnome.org/gtk-vnc :|
More information about the devel
mailing list