Searched refs:mkBitvector (Results 1 – 4 of 4) sorted by relevance
/netbsd-src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
H A D | SMTConv.h | 274 Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth), in fromCast() 275 Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth)); in fromCast() 395 Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); in getSymBinExpr() 403 Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); in getSymBinExpr() 498 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)), in getZeroExpr() 515 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); in getRangeExpr() 530 Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); in getRangeExpr()
|
H A D | SMTConstraintManager.h | 143 : Solver->mkBitvector(Value, Value.getBitWidth()), in REGISTER_TRAIT_WITH_PROGRAMSTATE()
|
/netbsd-src/external/apache2/llvm/dist/llvm/include/llvm/Support/ |
H A D | SMTAPI.h | 412 virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
|
/netbsd-src/external/apache2/llvm/dist/llvm/lib/Support/ |
H A D | Z3Solver.cpp | 726 SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override { in mkBitvector() function in __anondfffcc6f0111::Z3Solver 753 SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth()); in mkFloat()
|