martong marked 6 inline comments as done.
martong added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619-1620
+ const SymbolRef LHS = Sym->getLHS();
+ const llvm::APSInt &Zero =
+ Builder.getBasicValueFactory().getValue(0, Sym->getType());
+ // a % b != 0 implies that a != 0.
----------------
ASDenysPetrov wrote:
> Howerver, put this line inside //if-body// below, since `Zero` isn't needed
> wherever else.
Thanks, that is correct. I am going to address this in the child patch.
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627
+ const SymbolRef LHS = Sym->getLHS();
+ const llvm::APSInt &Zero =
+ Builder.getBasicValueFactory().getValue(0, Sym->getType());
+ // a % b != 0 implies that a != 0.
+ if (!Constraint.containsZero()) {
+ State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+ if (!State)
----------------
ASDenysPetrov wrote:
> martong wrote:
> > ASDenysPetrov wrote:
> > > How about using the family of `ProgramState::isNonNull` or
> > > `ProgramState::isNull` or `RangeConstraintManager::checkNull` functoins
> > > for this stuff?
> > I've been checking this and turend out that `ProgramState::isNull` does not
> > modify the State (this is aligned with being a `const` member function).
> > So, these functions do not "assume" anything, they can be used only to
> > query some property of an SVal (or Symbol) from the State.
> >
> > However, this comment and your other previous comment made me to do further
> > investigations towards exploiting the "assume" machinery better. The result
> > is a new child patch, where we can handle "adjustments" as well.
> But I don't see you use the modified `State` in any way. Why it's important
> for you to change the `State`?
>
>
> But I don't see you use the modified `State` in any way.
Actually, we do use it. The `State` we overwrite here is the member of the
class `ConstraintAssignor`, it is not a local variable.
> Why it's important for you to change the `State`?
It is important, because we'd like to assign new information to the existing
things we know (i.e. to the State). So, once we see a modulo then we can defer
some extra constraints and that is done via the `ConstraintAssignor`.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D110357/new/
https://reviews.llvm.org/D110357
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
