Page MenuHomePhabricator

[analyzer] Update SMT API documentation and methods
ClosedPublic

Authored by mikhail.ramalho on Jul 25 2018, 7:59 AM.

Details

Summary

Update the documentation of all the classes introduced with the new generic SMT API, most of them were referencing Z3 and how previous operations were being done (like including the context as parameter in a few methods).

Renamed the following methods, so it's clear that the operate on bitvectors:
*mkSignExt -> mkBVSignExt
*mkZeroExt -> mkBVZeroExt
*mkExtract -> mkBVExtract
*mkConcat -> mkBVConcat

Removed the unecessary methods:

  • getDataExpr: it was an one line method that called fromData
  • mkBitvector(const llvm::APSInt Int): it was not being used anywhere

Diff Detail

Repository
rL LLVM

Event Timeline

This revision is now accepted and ready to land.Jul 25 2018, 11:07 AM
This revision was automatically updated to reflect the committed changes.