[cfe-dev] Z3 constraint manager backend for Clang Static Analyzer

[Dominic Chen via cfe-dev]

I've just submitted a sequence of patches to the Clang static analyzer
that add additional support for reasoning about various symbolic
constraints and variables, using the Z3 theorem prover from Microsoft
Research. These are as follows:

* D28952: [analyzer] Add new Z3 constraint manager backend
* D28953: [analyzer] Eliminate analyzer limitations on symbolic
constraint generation
* D28954: [analyzer] Add support for symbolic float expressions
* D28955: [analyzer] Enable support for symbolic extension/truncation

I'd appreciate any input on this, since these are fairly large patches,
and there are still some outstanding issues. Namely, a couple of failing
testcases, updating the testsuite to account for differences in
capability between the two constraint solver backends, linking
dynamically against a 3rd party library, and some performance issues
with symbolic state explosion. These are discussed in more detail in the
body of D28952.

Thanks,

Dominic