[cfe-dev] clang vs llvm for verifying code

[Nuno Lopes]

Hi,

Next week I'm going to start to write a tool to verify the absence of buffer 
overflows in C code. I already wrote the backend (a model checker), but now 
I need a frontend to dump the states+transitions info.
My question is the following: should I dump this info directly from clang's 
AST or from LLVM bitcode? From what I understand, both have their advantages 
and disadvantages:

clang:
 + we're close to the source. it's easy to pinpoint the bug down to the line 
number
 + simple constant folding
 - AFAIK, merging the separate files' AST into a single, whole-program AST 
is not there yet. I may be able to merge the info later in the chain, 
though.
 - no (inter-procedural) alias analysis

llvm:
 + easy merging of the whole program into a single bitcode file
 + inter-procedural alias analysis. especially necessary for figuring out 
the callees of indirect function calls
 + possibility to run cheap optimizations to reduce the code size
 + the semantics of the C language are already lowered to simpler 
instructions
 - not clear to me if it's possible to accurately pinpoint the location of 
an error to the source program (maybe take advantage of the debug info?)

CIL:
 + seems to be used by many in the verification community
 + easy merging of the whole program AST
 + many different alias analysis algorithms
 - no C++ support
 - written in ocaml... bah!

Does anyone has any other point to add? Any recommendation?

Thanks,
Nuno