[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Ryan Govostes via Phabricator via cfe-commits]

rgov added a comment.

Do you think you could upload the patch omitting all of the test case changes 
for now? Maybe include one as an example but it seems to be just adding 
`%z3_cc1` so we don't need to see all of them right now.

The KLEE project has a useful abstraction layer around multiple bitvector 
solvers (Boolector, CVC4, STP, and Z3). It's also used by Souper, another 
LLVM-based project. I would encourage you to consider using that rather than 
interacting directly with a specific solver.

For what it's worth, here's my attempt 

 at integrating STP.


https://reviews.llvm.org/D28952



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28955: [analyzer] Enable support for symbolic extension/truncation

[Ryan Govostes via Phabricator via cfe-commits]

rgov added a comment.

Are all the changes here related to the extension/truncation support, for 
instance the changes to `test/Analysis/malloc.c`? Can you move misc. cleanup 
changes to another review?


https://reviews.llvm.org/D28955



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits