Erik de Castro Lopo <mle+s...@mega-nerd.com> writes: > Daniel Pittman wrote:
[...] >> In the bigger picture, your original question about static analysis >> tools for C missed one critical detail: what do you actually want it to >> statically analyse? > > I'm the author of libsndfile: > > http://www.mega-nerd.com/libsndfile/ > > which is a library for reading and writing sound files. These sound > files have to be considered untrusted (ie downloaded from the big > bad internet). > > In addition, most sound files types have binary 16 and 32 bit integer > values in their headers which then need to be used as things like indexes > into arrays. > > Obviously, values retrieved from an untrusted source need to be validated > before they are used but its very easy to forget. I'd like to have a > static analyser that can tell me when a untrusted value is used before it > is validated. *nod* You might find sparse works well for you, then: one of the key features it supports is tagging values into different data "spaces", incompatible with each other. You could use this to tag values read from the file as untrusted, and forcibly convert them into trusted values in your "boundary check and validate" routines.[1] This approach is used in the Linux kernel, where sparse originated, to differentiate between user and kernel pointers, among other things, for the same sort of validation you are talking about. Regards, Daniel Footnotes: [1] I am assuming your model is the traditional "soft in the middle" strategy of read, validate and then trust the pointer without actually checking this. _______________________________________________ coders mailing list coders@slug.org.au http://lists.slug.org.au/listinfo/coders