This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Create generic SMT Sort Class
ClosedPublic

Authored by mikhail.ramalho on Jul 19 2018, 9:09 AM.

Details

Summary

New base class for all future SMT sorts.

The only change is that the class implements methods isBooleanSort(), isBitvectorSort() and isFloatSort() so it doesn't rely on Z3's enum.

Diff Detail

Event Timeline

Make some methods pure virtual

george.karpenkov requested changes to this revision.Jul 20 2018, 10:15 AM

Small change requested. Otherwise, good to go.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
64

A reference to a generic SMTContext is not very useful.
Could we just remove that, then you can remove the constructor of SMTContext,
just store Z3Context in a subclass, and then you won't need casts everywhere as well?

This revision now requires changes to proceed.Jul 20 2018, 10:15 AM

Removed SMTContext reference from SMTSort.

This revision is now accepted and ready to land.Jul 23 2018, 10:43 AM
This revision was automatically updated to reflect the committed changes.