Page MenuHomePhabricator

[analyzer] Cleanup constructors in the Z3 backend

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



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

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)

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.
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.