14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==// 24502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 34502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// The LLVM Compiler Infrastructure 44502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 54502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// This file is distributed under the University of Illinois Open Source 64502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// License. See LICENSE.TXT for details. 74502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 84502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===// 94502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// Code shared between BasicConstraintManager and RangeConstraintManager. 114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===// 134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 145a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#ifndef LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H 155a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#define LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H 164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" 1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 229ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 235a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekclass SimpleConstraintManager : public ConstraintManager { 25ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose SubEngine *SU; 261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF; 274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 28ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose SimpleConstraintManager(SubEngine *subengine, BasicValueFactory &BV) 291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose : SU(subengine), BVF(BV) {} 301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump virtual ~SimpleConstraintManager(); 311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 32a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 33a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Common implementation for the interface provided by ConstraintManager. 34a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 35f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek 368bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, 375b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption); 38f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek 398bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assume(ProgramStateRef state, Loc Cond, bool Assumption); 404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 418bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption); 424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 438bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymRel(ProgramStateRef state, 44ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 45ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 46ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int); 471eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 48a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekprotected: 491eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 50a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 51a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Interface that subclasses must implement. 52a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 54ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison 55ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // operation for the method being invoked. 568bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym, 57ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 58ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 608bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym, 61ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 62ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 648bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym, 65ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 66ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 688bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym, 69ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 70ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 728bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym, 73ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 74ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 768bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym, 77ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 78ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 791eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 80a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 81a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Internal implementation. 82a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &getBasicVals() const { return BVF; } 851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 86eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaks bool canReasonAbout(SVal X) const; 87eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaks 888bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeAux(ProgramStateRef state, 893cdf584e068056540769dab56cad333e95a89750Anna Zaks Loc Cond, 903cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption); 911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 928bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeAux(ProgramStateRef state, 933cdf584e068056540769dab56cad333e95a89750Anna Zaks NonLoc Cond, 943cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption); 953cdf584e068056540769dab56cad333e95a89750Anna Zaks 968bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeAuxForSymbol(ProgramStateRef State, 973cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef Sym, 983cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption); 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1015a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace 1025a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 1035a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end clang namespace 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 105669c0e13d3ab342f9b074a8c3eeeb887cf54b52fTed Kremenek#endif 106