Could we generate equivalent C code and then use a C analyzer?
How can we achieve concolic execution (instrumented symbolic execution at runtime by generating random values that force one or another branch to visit every part of a function's possible graph of paths)?
Since we're building on top of LLVM, we may be able to use KLEE (http://klee.github.io/). Other sources: http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2010_dynamic-abstract.html, http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext.
Could we generate equivalent C code and then use a C analyzer?
How can we achieve concolic execution (instrumented symbolic execution at runtime by generating random values that force one or another branch to visit every part of a function's possible graph of paths)?