Commit Graph

3 Commits

Author SHA1 Message Date
Dominic Chen c0402c6916 Revert "[analyzer] Support generating and reasoning over more symbolic constraint types"
Assertion `Loc::isLocType(SSE->getLHS()->getType())' failed in Analysis/PR3991.m

This reverts commit e469ff2759275e67f9072b3d67fac90f647c0fe6.

llvm-svn: 307853
2017-07-12 21:43:42 +00:00
Dominic Chen 35610d21b2 [analyzer] Support generating and reasoning over more symbolic constraint types
Summary: Generate more IntSymExpr constraints, perform SVal simplification for IntSymExpr and SymbolCast constraints, and create fully symbolic SymExprs

Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun

Subscribers: mgorny, cfe-commits

Differential Revision: https://reviews.llvm.org/D28953

llvm-svn: 307833
2017-07-12 19:37:57 +00:00
Dominic Chen 08f943c563 [analyzer] Add new Z3 constraint manager backend
Summary: Implement new Z3 constraint manager backend.

Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun

Subscribers: mgorny, cfe-commits

Differential Revision: https://reviews.llvm.org/D28952

llvm-svn: 299463
2017-04-04 19:52:25 +00:00