cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT

Browse Source
This commit is contained in:
Martin Blicha 2021-01-14 13:31:30 +01:00
parent 2a62814686
commit 32a923c7ef
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/SymbolicState.cpp
View File

@ -264,14 +264,14 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
/// Otherwise we create a tuple wrapping the necessary input or output types. /// Otherwise we create a tuple wrapping the necessary input or output types.
auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> { auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> {
if (_types.size() == 1) if (_types.size() == 1)
return smtSort(*_types.front()); return smtSortAbstractFunction(*_types.front());
vector<string> inNames; vector<string> inNames;
vector<SortPointer> sorts; vector<SortPointer> sorts;
for (unsigned i = 0; i < _types.size(); ++i) for (unsigned i = 0; i < _types.size(); ++i)
{ {
inNames.emplace_back(_name + "_input_" + to_string(i)); inNames.emplace_back(_name + "_input_" + to_string(i));
sorts.emplace_back(smtSort(*_types.at(i))); sorts.emplace_back(smtSortAbstractFunction(*_types.at(i)));
} }
return make_shared<smtutil::TupleSort>( return make_shared<smtutil::TupleSort>(
_name + "_input", _name + "_input",