r344463 - [analyzer] Small SMT API improvement

Enrico Steffinlongo via cfe-commits cfe-commits at lists.llvm.org
Sat Oct 13 12:42:10 PDT 2018


Author: esteffin
Date: Sat Oct 13 12:42:10 2018
New Revision: 344463

URL: http://llvm.org/viewvc/llvm-project?rev=344463&view=rev
Log:
[analyzer] Small SMT API improvement

Summary: Removed const qualifier from reset method of SMTSolver and Z3Solver objects.

Reviewers: mikhail.ramalho, george.karpenkov, NoQ, ddcc

Reviewed By: NoQ

Subscribers: xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D52031

Modified:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
    cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=344463&r1=344462&r2=344463&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Sat Oct 13 12:42:10 2018
@@ -283,7 +283,7 @@ public:
   virtual void pop(unsigned NumStates = 1) = 0;
 
   /// Reset the solver and remove all constraints.
-  virtual void reset() const = 0;
+  virtual void reset() = 0;
 
   virtual void print(raw_ostream &OS) const = 0;
 };

Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=344463&r1=344462&r2=344463&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Sat Oct 13 12:42:10 2018
@@ -859,7 +859,7 @@ public:
   }
 
   /// Reset the solver and remove all constraints.
-  void reset() const override { Z3_solver_reset(Context.Context, Solver); }
+  void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);




More information about the cfe-commits mailing list