clang  6.0.0svn
SimpleConstraintManager.h
Go to the documentation of this file.
1 //== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
2 //
3 // The LLVM Compiler Infrastructure
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 //
10 // Simplified constraint manager backend.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
16 
19 
20 namespace clang {
21 
22 namespace ento {
23 
25  SubEngine *SU;
26  SValBuilder &SVB;
27 
28 public:
30  : SU(subengine), SVB(SB) {}
31 
32  ~SimpleConstraintManager() override;
33 
34  //===------------------------------------------------------------------===//
35  // Implementation for interface from ConstraintManager.
36  //===------------------------------------------------------------------===//
37 
38  /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
39  /// creating boolean casts to handle Loc's.
41  bool Assumption) override;
42 
44  const llvm::APSInt &From,
45  const llvm::APSInt &To,
46  bool InRange) override;
47 
48 protected:
49  //===------------------------------------------------------------------===//
50  // Interface that subclasses must implement.
51  //===------------------------------------------------------------------===//
52 
53  /// Given a symbolic expression that can be reasoned about, assume that it is
54  /// true/false and generate the new program state.
56  bool Assumption) = 0;
57 
58  /// Given a symbolic expression within the range [From, To], assume that it is
59  /// true/false and generate the new program state.
60  /// This function is used to handle case ranges produced by a language
61  /// extension for switch case statements.
63  SymbolRef Sym,
64  const llvm::APSInt &From,
65  const llvm::APSInt &To,
66  bool InRange) = 0;
67 
68  /// Given a symbolic expression that cannot be reasoned about, assume that
69  /// it is zero/nonzero and add it directly to the solver state.
71  SymbolRef Sym,
72  bool Assumption) = 0;
73 
74  //===------------------------------------------------------------------===//
75  // Internal implementation.
76  //===------------------------------------------------------------------===//
77 
79  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
80 
81 private:
82  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
83 
84  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
85  bool Assumption);
86 };
87 
88 } // end GR namespace
89 
90 } // end clang namespace
91 
92 #endif
SymbolManager & getSymbolManager()
Definition: SValBuilder.h:147
virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
Symbolic value.
Definition: SymExpr.h:29
LineState State
SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
BasicValueFactory & getBasicVals() const
ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle...
virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
Dataflow Directional Tag Classes.
BasicValueFactory & getBasicValueFactory()
Definition: SValBuilder.h:144