ConstraintManager() = default;
virtual ~ConstraintManager();
+ virtual bool haveEqualConstraints(ProgramStateRef S1,
+ ProgramStateRef S2) const = 0;
+
virtual ProgramStateRef assume(ProgramStateRef state,
DefinedSVal Cond,
bool Assumption) = 0;
ProgramStateRef getPersistentStateWithGDM(ProgramStateRef FromState,
ProgramStateRef GDMState);
- bool haveEqualEnvironments(ProgramStateRef S1, ProgramStateRef S2) {
+ bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const {
+ return ConstraintMgr->haveEqualConstraints(S1, S2);
+ }
+
+ bool haveEqualEnvironments(ProgramStateRef S1, ProgramStateRef S2) const {
return S1->Env == S2->Env;
}
- bool haveEqualStores(ProgramStateRef S1, ProgramStateRef S2) {
+ bool haveEqualStores(ProgramStateRef S1, ProgramStateRef S2) const {
return S1->store == S2->store;
}
OS << nl;
}
+ bool haveEqualConstraints(ProgramStateRef S1,
+ ProgramStateRef S2) const override {
+ return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
+ }
+
bool canReasonAbout(SVal X) const override {
const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
BugReporterContext &BRC, BugReport &BR) {
ProgramPoint progPoint = N->getLocation();
ProgramStateRef CurrentState = N->getState();
- ProgramStateRef PrevState = N->getFirstPred()->getState();
+ ProgramStateRef PreviousState = N->getFirstPred()->getState();
- // Compare the GDMs of the state, because that is where constraints
- // are managed. Note that ensure that we only look at nodes that
- // were generated by the analyzer engine proper, not checkers.
- if (CurrentState->getGDM().getRoot() ==
- PrevState->getGDM().getRoot())
+ // If the constraint information does not changed there is no assumption.
+ if (BRC.getStateManager().haveEqualConstraints(CurrentState, PreviousState))
return nullptr;
// If an assumption was made on a branch, it should be caught
break;
}
+ Cond = Cond->IgnoreParens();
+
// However, when we encounter a logical operator as a branch condition,
// then the condition is actually its RHS, because LHS would be
// the condition for the logical operator terminator.
// Implementation for interface from ConstraintManager.
//===------------------------------------------------------------------===//
+ bool haveEqualConstraints(ProgramStateRef S1,
+ ProgramStateRef S2) const override {
+ return S1->get<ConstraintRange>() == S2->get<ConstraintRange>();
+ }
+
bool canReasonAbout(SVal X) const override;
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;