Searched refs:mkBitvector (Results 1 – 4 of 4) sorted by relevance
| /freebsd-12.1/contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 271 Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth), in fromCast() 272 Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth)); in fromCast() 382 SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); in getSymBinExpr() 389 SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); in getSymBinExpr() 482 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)), in getZeroExpr() 499 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); in getRangeExpr() 513 SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); in getRangeExpr()
|
| H A D | SMTSolver.h | 267 virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
|
| H A D | SMTConstraintManager.h | 138 : Solver->mkBitvector(Value, Value.getBitWidth()), in getSymVal()
|
| /freebsd-12.1/contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/ |
| H A D | Z3ConstraintManager.cpp | 650 SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override { in mkBitvector() function in __anon1f86e14b0211::Z3Solver 662 SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth()); in mkFloat()
|