This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Cleanup constructors in the Z3 backend
ClosedPublic

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

Details

Summary

Left only the constructors that are actually required, and marked the move constructors as deleted. They are not used anymore and we were never sure they've actually worked correctly.

Diff Detail

Repository
rC Clang

Event Timeline

george.karpenkov accepted this revision.Nov 27 2018, 2:19 PM

I'm OK with the change; not sure why you've decided to remove a creator for a model (it should probably have a different name though)

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
80 ↗(On Diff #175577)

TBH I have no idea what calling SMTSort with no argument does.
Same as not doing anything?

859 ↗(On Diff #175577)

Should this be removed?

This revision is now accepted and ready to land.Nov 27 2018, 2:19 PM
mikhail.ramalho marked 2 inline comments as done.Nov 27 2018, 2:46 PM
mikhail.ramalho added inline comments.
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
80 ↗(On Diff #175577)

If there is no call to the base class constructor, the compiler will insert a call to the base class with no argument.

But yeah, the SMTSort constructor doesn't initialize anything.

859 ↗(On Diff #175577)

Yep, the getModel method is not part of the API, it's Z3 specific. No point in keeping it around.

This revision was automatically updated to reflect the committed changes.