Skip to content
Commit 32ce136e authored by Mikhail R. Gadelha's avatar Mikhail R. Gadelha
Browse files

[analyzer] Improvements to the SMT API

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.

Reviewers: george.karpenkov, NoQ

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D52365

llvm-svn: 343581
parent 74028360
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment