martong added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2822
PathSensitiveBugReport &BR) {
// Collect new constraints
+ addConstraints(EndPathNode, /*OnlyForNewSymbols=*/false);
----------------
Probably you wanted to use `hasContradictionUsingZ3` starting from here. (?)
================
Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2871
+ // Overwrite the associated constraint of the Symbol.
+ Constraints = CF.remove(Constraints, Sym);
Constraints = CF.add(Constraints, Sym, C.second);
----------------
steakhal wrote:
> How can we simplify this?
Could we change the visitation logic to start with the `EndPathNode`? I mean
could we exercise `FalsePositiveRefutationBRVisitor` to start the visitation
from `EndPathNode`? If that was possible then this whole patch would be way
simpler.
In BugReporter.cpp:
```
// Run visitors on all nodes starting from the node *before* the last one.
// The last node is reserved for notes generated with {@code getEndPath}.
const ExplodedNode *NextNode = ErrorNode->getFirstPred();
while (NextNode) {
```
Why can't we have a different visitation order implemented specifically for the
refutation visitor? (@NoQ, @xazax.hun)
================
Comment at:
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp:194
+ // This assumption is false!
+ // 'y' can not be 5 if the maximal value of both x and y is 2.
+ // This bugreport must be caught by the visitor, since the
constraints
----------------
`x and y` -> `x and n`.
================
Comment at:
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp:197
+ // of the bugpath are UnSAT.
+ reportIfCanBeZero(y - 5);
+ }
----------------
Perhaps `reportIfTrue(y > 4)` would be easier to understand here. But then
probably you also need a rename: `ZERO_STATE_SHOULD_NOT_EXIST` ->
`STATE_SHOULD_NOT_EXIST`
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D78457/new/
https://reviews.llvm.org/D78457
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
