summaryrefslogtreecommitdiffstats
path: root/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Commit message (Expand)AuthorAgeFilesLines
* This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.Mikhail R. Gadelha2019-02-091-0/+835
* Move the SMT API to LLVMMikhail R. Gadelha2019-02-071-835/+0
* Got rid of the `Z3ConstraintManager` classMikhail R. Gadelha2019-02-071-16/+1
* Generalised the SMT state constraintsMikhail R. Gadelha2019-02-071-26/+36
* Update the file headers across all of the LLVM projects in the monorepoChandler Carruth2019-01-191-4/+3
* [analyzer] Cleanup constructors in the Z3 backendMikhail R. Gadelha2018-11-281-96/+31
* Fix compatibility with z3-4.8.1Jan Kratochvil2018-11-121-1/+1
* [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManagerMikhail R. Gadelha2018-10-251-43/+2
* [analyzer] Fixed bitvector from model always being unsignedMikhail R. Gadelha2018-10-251-3/+5
* [analyzer] Improved cmake configuration for Z3Enrico Steffinlongo2018-10-131-2/+2
* [analyzer] Small SMT API improvementEnrico Steffinlongo2018-10-131-1/+1
* [analyzer] Improvements to the SMT APIMikhail R. Gadelha2018-10-021-34/+4
* [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. ...Mikhail R. Gadelha2018-08-231-12/+4
* [analyzer] Templatefy SMTConstraintManager so more generic code can be moved ...Mikhail R. Gadelha2018-08-231-58/+1
* [analyzer] Delete SMTContext. NFC.Mikhail R. Gadelha2018-08-231-3/+2
* [analyzer] Fixed method to get APSInt modelMikhail R. Gadelha2018-07-261-23/+18
* [analyzer] Update SMT API documentation and methodsMikhail R. Gadelha2018-07-251-19/+13
* [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backendMikhail R. Gadelha2018-07-251-22/+7
* [analyzer] Removed API used by the Refutation Manager from SMTConstraintManag...Mikhail R. Gadelha2018-07-251-1/+12
* [analyzer] Moved non solver specific code from Z3ConstraintManager to SMTCons...Mikhail R. Gadelha2018-07-251-765/+72
* [analyzer] Implemented SMT generic APIMikhail R. Gadelha2018-07-251-545/+569
* [analyzer] Create generic SMT Expr classMikhail R. Gadelha2018-07-251-53/+44
* [analyzer] Create generic SMT Sort ClassMikhail R. Gadelha2018-07-251-25/+29
* [analyzer] Moved static Context to class memberMikhail R. Gadelha2018-07-251-450/+471
* [analyzer] Create generic SMT Context classMikhail R. Gadelha2018-07-251-6/+10
* [analyzer] Fix Z3 backend after D48205Mikhail R. Gadelha2018-07-171-30/+29
* [analyzer] Fix the Z3 backend always generating unsigned APSIntMikhail R. Gadelha2018-07-161-3/+5
* [analyzer] Fix wrong comparison generation of the ranges generated by the ref...Mikhail R. Gadelha2018-06-281-3/+2
* [analyzer] Optimize constraint generation when the range is a concrete valueMikhail R. Gadelha2018-06-201-52/+47
* [analyzer] Add method to the generic SMT API to dump the SMT formulaMikhail R. Gadelha2018-06-161-0/+7
* [Analyzer] Fix Z3ConstraintManager crash (PR37646)Vlad Tsyrklevich2018-06-061-2/+4
* Created a tiny SMT interface and make Z3ConstraintManager implement itMikhail R. Gadelha2018-06-041-3/+58
* [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManagerDominic Chen2018-05-311-22/+50
* Revert "[analyzer] Support generating and reasoning over more symbolic constr...Dominic Chen2017-07-121-18/+9
* [analyzer] Support generating and reasoning over more symbolic constraint typesDominic Chen2017-07-121-9/+18
* [analyzer] Add new Z3 constraint manager backendDominic Chen2017-04-041-0/+1618
OpenPOWER on IntegriCloud