Page MenuHomePhabricator

[analyzer] Got rid of the `Z3ConstraintManager` class
ClosedPublic

Authored by mikhail.ramalho on Nov 27 2018, 2:33 PM.

Details

Summary

Now, instead of passing the reference to a shared_ptr, we pass the shared_ptr instead.

I've also removed the check if Z3 is present in CreateZ3ConstraintManager as this function already calls CreateZ3Solver that performs the exactly same check.

Diff Detail

Repository
rC Clang

Event Timeline

Moved CreateZ3Solver to SMTConstraintManager.

In the future, CreateZ3Solver should be renamed CreateSMTSolver to handle all backends.

NoQ accepted this revision.Nov 30 2018, 5:27 PM

Makes perfect sense to me.

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
834 ↗(On Diff #176119)

Why are we even passing StMgr into this callback when it can be easily retrieved from Eng? :)

This revision is now accepted and ready to land.Nov 30 2018, 5:27 PM
mikhail.ramalho marked an inline comment as done.Dec 10 2018, 12:20 PM
mikhail.ramalho added inline comments.
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
834 ↗(On Diff #176119)

I guess I simply copied it from RangeConstraintManager.cpp:311...

I can send another patch to remove the parameter from both functions. They are declared in ConstraintManager.h:200 and ConstraintManager.h:204.

Closed by commit rC353371: Got rid of the `Z3ConstraintManager` class (authored by mramalho, committed by ). · Explain WhyFeb 6 2019, 7:18 PM
This revision was automatically updated to reflect the committed changes.
Herald added a project: Restricted Project. · View Herald TranscriptFeb 6 2019, 7:18 PM
Herald added a subscriber: cfe-commits. · View Herald Transcript