diff options
Diffstat (limited to 'libsolidity/formal/SymbolicTypes.cpp')
| -rw-r--r-- | libsolidity/formal/SymbolicTypes.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index a3b6e3a8..2d0107c5 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -32,10 +32,29 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type) return make_shared<smt::Sort>(smt::Kind::Int); case smt::Kind::Bool: return make_shared<smt::Sort>(smt::Kind::Bool); + case smt::Kind::Function: + { + auto fType = dynamic_cast<FunctionType const*>(&_type); + solAssert(fType, ""); + vector<smt::SortPointer> parameterSorts = smtSort(fType->parameterTypes()); + auto returnTypes = fType->returnParameterTypes(); + // TODO remove this when we support tuples. + solAssert(returnTypes.size() == 1, ""); + smt::SortPointer returnSort = smtSort(*returnTypes.at(0)); + return make_shared<smt::FunctionSort>(parameterSorts, returnSort); + } } solAssert(false, "Invalid type"); } +vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types) +{ + vector<smt::SortPointer> sorts; + for (auto const& type: _types) + sorts.push_back(smtSort(*type)); + return sorts; +} + smt::Kind dev::solidity::smtKind(Type::Category _category) { if (isNumber(_category)) |