clang: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Source File (original) (raw)

1

2

3

4

5

6

7

8

9

10

11

12

13

17#include

18

20

21namespace ento {

22

24

27 bool Assumption) {

28

29 if (std::optional LV = Cond.getAs<Loc>()) {

32 const MemRegion *MR = LV->getAsRegion();

33 if (const TypedRegion *TR = dyn_cast_or_null(MR))

34 T = TR->getLocationType();

35 else

36 T = SVB.getContext().VoidPtrTy;

37

38 Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();

39 }

40

41 return assume(State, Cond.castAs<NonLoc>(), Assumption);

42}

43

46 State = assumeAux(State, Cond, Assumption);

47 if (EE)

49 return State;

50}

51

54 bool Assumption) {

55

56

57

59

61 assert(Sym);

63 }

64

65 switch (Cond.getKind()) {

66 default:

67 llvm_unreachable("'Assume' not implemented for this NonLoc");

68

69 case nonloc::SymbolValKind: {

70 nonloc::SymbolVal SV = Cond.castAsnonloc::SymbolVal();

72 assert(Sym);

73 return assumeSym(State, Sym, Assumption);

74 }

75

76 case nonloc::ConcreteIntKind: {

77 bool b = *Cond.castAsnonloc::ConcreteInt().getValue() != 0;

78 bool isFeasible = b ? Assumption : !Assumption;

79 return isFeasible ? State : nullptr;

80 }

81

82 case nonloc::PointerToMemberKind: {

83 bool IsNull = Cond.castAsnonloc::PointerToMember().isNullMemberPointer();

84 bool IsFeasible = IsNull ? Assumption : !Assumption;

85 return IsFeasible ? State : nullptr;

86 }

87

88 case nonloc::LocAsIntegerKind:

89 return assumeInternal(State, Cond.castAsnonloc::LocAsInteger().getLoc(),

90 Assumption);

91 }

92}

93

96 const llvm::APSInt &To, bool InRange) {

97

98 assert(From.isUnsigned() == To.isUnsigned() &&

99 From.getBitWidth() == To.getBitWidth() &&

100 "Values should have same types!");

101

103

105 assert(Sym);

107 }

108

110 default:

111 llvm_unreachable("'assumeInclusiveRange' is not implemented"

112 "for this NonLoc");

113

114 case nonloc::LocAsIntegerKind:

115 case nonloc::SymbolValKind: {

118 return State;

119 }

120

121 case nonloc::ConcreteIntKind: {

123 bool IsInRange = IntVal >= From && IntVal <= To;

124 bool isFeasible = (IsInRange == InRange);

125 return isFeasible ? State : nullptr;

126 }

127 }

128}

129

130}

131

132}

A (possibly-)qualified type.

virtual bool canReasonAbout(SVal X) const =0

canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.

ProgramStateRef processAssume(ProgramStateRef state, SVal cond, bool assumption)

evalAssume - Callback function invoked by the ConstraintManager when making assumptions about state v...

MemRegion - The root abstract class for all memory regions.

SValBuilder & getSValBuilder()

ProgramStateManager & getStateManager()

ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override

Definition SimpleConstraintManager.cpp:94

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...

~SimpleConstraintManager() override

Definition SimpleConstraintManager.cpp:23

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 ...

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...

ProgramStateRef assumeInternal(ProgramStateRef State, DefinedSVal Cond, bool Assumption) override

Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle...

Definition SimpleConstraintManager.cpp:25

TypedRegion - An abstract class representing regions that are typed.

Value representing integer constant.

IntrusiveRefCntPtr< const ProgramState > ProgramStateRef

const SymExpr * SymbolRef

The JSON file list parser is used to communicate input to InstallAPI.

const FunctionProtoType * T