This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Improvements to the SMT API
ClosedPublic

Authored by mikhail.ramalho on Sep 21 2018, 10:22 AM.

Details

Summary

Several improvements in preparation for the new backends.

Refactoring:

  • Removed duplicated methods fromBoolean, fromAPSInt, fromInt and fromAPFloat. The methods mkBoolean, mkBitvector and mkFloat are now used instead.
  • The names of the functions that convert BVs to FPs were swapped (mkSBVtoFP, mkUBVtoFP, mkFPtoSBV, mkFPtoUBV).
  • Added a couple of comments in function calls.

Crosscheck encoding:

  • Changed how constraints are encoded in the refutation manager so it doesn't start with (false OR ...). This change introduces one duplicated line (see file BugReporterVisitors.cpp, the `SMTConv::getRangeExpr is called twice, so I can remove this change if the duplication is a problem.

Diff Detail

Event Timeline

george.karpenkov accepted this revision.Sep 21 2018, 1:26 PM
This revision is now accepted and ready to land.Sep 21 2018, 1:26 PM
This revision was automatically updated to reflect the committed changes.