george.karpenkov added inline comments.
================ Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:496 std::unique_ptr<ConstraintManager> ConstraintMgr; + std::unique_ptr<ConstraintManager> RefutationMgr; ---------------- See the comment below, I think we should not have this manager here. Just create one in the visitor constructor. ================ Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:563 + + ConstraintManager& getRefutationManager() { + return *RefutationMgr; ---------------- This should be deleted as well (see the comment above) ================ Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 + // Reset the solver + RefutationMgr.reset(); + } ---------------- george.karpenkov wrote: > (apologies in advance for nitpicking not on your code). > > Currently, this is written in a stateful way: we have a solver, at each > iteration we add constraints, and at the end we reset it. To me it would make > considerably more sense to write the code in a functional style: as we go, > generate a vector of formulas, then once we reach the path end, create the > solver object, check satisfiability, and then destroy the entire solver. Elaborating more: we are already forced to have visitor object state, let's use that. `RefutationMgr` is essentially a wrapper around a Z3 solver object, let's just create one when visitor is constructed (directly or in unique_ptr) and then rely on the destructor to destroy it. Then no `reset` is necessary. ================ Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:83 ConstraintMgr = (*CreateCMgr)(*this, SubEng); + AnalyzerOptions &Opts = SubEng->getAnalysisManager().getAnalyzerOptions(); + RefutationMgr = Opts.shouldCrosscheckWithZ3() ---------------- This could be removed as well (see the comment above) ================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:919 + void reset() override; + ---------------- `reset` should be removed, see comments above. ================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1246 +void Z3ConstraintManager::reset() { Solver.reset(); } + ---------------- I would remove this, see comments above. ================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292 + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); + } ---------------- I'm very confused as to why are we doing disjunctions here. https://reviews.llvm.org/D45517 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits