danix800 added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:192-198
+ SVal Count = CE.getArgSVal(0);
+ for (size_t i = 0; i < ArrSize; ++i) {
+ const NonLoc Idx = Ctx.getSValBuilder().makeArrayIndex(i);
+ auto CountReached = SVB.evalBinOp(State, BO_GE, Idx, Count,
ASTCtx.BoolTy)
+ .getAs<DefinedOrUnknownSVal>();
+ if (CountReached && State->assume(*CountReached, true))
+ break;
----------------
steakhal wrote:
> It's suspicious to me to compare stuff in the symbolic domain, such as `Idx
> >= Count` here.
> And let me elaborate on why I think so.
>
> I'd assume that the first argument of `MPI_Waitall` is usually just a number
> literal, thus it's gonna be a ConcreteInt, so now we have `Count`.
> The `Index` you just created, obviously is just a ConcreteInt.
> After this, we could simply unwrap them and do the comparison without doing
> it in the symbolic domain.
>
> ---
>
> As a sidenote, `State->assume(*CountReached, true)` would return a state in
> two cases:
> 1) We can prove that the assumption holds.
> 2) We cannot disprove the assumption, thus it might hold, so we assume it
> holds.
> This is probably not what you wanted in the first place, but it's probably
> irrelelevant anyway.
I'll restrict this checker to handle `ConcreteInt` count only.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D158813/new/
https://reviews.llvm.org/D158813
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
