aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-11-30 23:48:46 +0800
committerGitHub <noreply@github.com>2018-11-30 23:48:46 +0800
commitcc00d8172b6cd7f9fc032e4a21857455ace2f290 (patch)
tree6dbb7559833533ed81975ea3ee1ca6cf03515eb8 /libsolidity
parenteea8cecd42a3abe22bdcf207ee4364f2b7a17b08 (diff)
parent2f6de12e8ca98c92ee708081c3a3be05c2c30c6c (diff)
downloaddexon-solidity-cc00d8172b6cd7f9fc032e4a21857455ace2f290.tar.gz
dexon-solidity-cc00d8172b6cd7f9fc032e4a21857455ace2f290.tar.zst
dexon-solidity-cc00d8172b6cd7f9fc032e4a21857455ace2f290.zip
Merge pull request #5528 from ethereum/smt_sorts_virtual
[SMTChecker] Make smt::Sort::operator== virtual
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SolverInterface.h22
1 files changed, 16 insertions, 6 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 7f20876e..4a4b3fb1 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -55,7 +55,7 @@ struct Sort
Sort(Kind _kind):
kind(_kind) {}
virtual ~Sort() = default;
- bool operator==(Sort const& _other) const { return kind == _other.kind; }
+ virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
Kind const kind;
};
@@ -65,16 +65,22 @@ struct FunctionSort: public Sort
{
FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
- bool operator==(FunctionSort const& _other) const
+ bool operator==(Sort const& _other) const override
{
+ if (!Sort::operator==(_other))
+ return false;
+ auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
+ solAssert(_otherFunction, "");
+ if (domain.size() != _otherFunction->domain.size())
+ return false;
if (!std::equal(
domain.begin(),
domain.end(),
- _other.domain.begin(),
+ _otherFunction->domain.begin(),
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
))
return false;
- return Sort::operator==(_other) && *codomain == *_other.codomain;
+ return *codomain == *_otherFunction->codomain;
}
std::vector<SortPointer> domain;
@@ -87,9 +93,13 @@ struct ArraySort: public Sort
/// _range is the sort of the values
ArraySort(SortPointer _domain, SortPointer _range):
Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
- bool operator==(ArraySort const& _other) const
+ bool operator==(Sort const& _other) const override
{
- return Sort::operator==(_other) && *domain == *_other.domain && *range == *_other.range;
+ if (!Sort::operator==(_other))
+ return false;
+ auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
+ solAssert(_otherArray, "");
+ return *domain == *_otherArray->domain && *range == *_otherArray->range;
}
SortPointer domain;