Dominic Chen
cd81614e8b
[analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager
...
Summary: Clang does not have a corresponding QualType for a 1-bit APSInt, so use the BoolTy and extend the APSInt. Split from D35450. Fixes PR37622.
Reviewers: george.karpenkov, NoQ
Subscribers: mikhail.ramalho, xazax.hun, szepet, rnkovacs, cfe-commits, a.sidorin
Differential Revision: https://reviews.llvm.org/D47603
llvm-svn: 333704
2018-05-31 22:23:07 +00:00
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
