Need assistance using Clang for integer and buffer range constraints generation

Hello all,

I’m an undergraduate CS student at the Technion IIT, and I’m working with a small team on an academic project in which we want to find buffer overruns statically.

For that purpose we plan to initially implement the method described by Ganapathy et al. at http://www.cs.wisc.edu/wisa/papers/ccs03/p351-ganapathy.pdf, and to do that we want to use Clang.

The output we need per source file is a list of linear constraints on integers and on char arrays, giving us the minimal and maximal value of each integer, and the minimal and maximal size of an allocated buffer.
I’m having a bit of a hard time ramping up on using Clang to achieve this, which is why I’m asking this list for help - What would be the best approach for this, should we hook into the static analyzer and generate the constraints ourselves, or is there a way to receive such constraints from the code that already exists in clang?

I’d very much appreciate any pointers to information and examples that can assist us, either on- or off-list.

Thanks in advance,