diff options
| author | chriseth <chris@ethereum.org> | 2017-09-28 17:29:04 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2017-10-18 01:29:53 +0800 |
| commit | 1f97c1ea8fec9a755d767811731f57fd527747b5 (patch) | |
| tree | 064601c3395fdadef118968950b42a5dd3d3fe20 /libsolidity/formal | |
| parent | 846b43479dc2991fbbab8b497a622fd58204e08e (diff) | |
| download | dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar.gz dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar.bz2 dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar.lz dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar.xz dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.tar.zst dexon-solidity-1f97c1ea8fec9a755d767811731f57fd527747b5.zip | |
Rename variables in SMT checker.
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 18 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
2 files changed, 11 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 7c8c089e..2d2f05ec 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo { solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); - solAssert(m_Variables.count(&_varDecl) == 0, ""); + solAssert(m_variables.count(&_varDecl) == 0, ""); m_currentSequenceCounter[&_varDecl] = 0; m_nextFreeSequenceCounter[&_varDecl] = 1; - m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); setValue(_varDecl, _setToZero); } else @@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!m_Expressions.count(&_e)) + if (!m_expressions.count(&_e)) { solAssert(_e.annotation().type, ""); switch (_e.annotation().type->category()) @@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e) { if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) solAssert(!rational->isFractional(), ""); - m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; } case Type::Category::Integer: - m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; case Type::Category::Bool: - m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); break; default: solAssert(false, "Type not implemented."); } } - return m_Expressions.at(&_e); + return m_expressions.at(&_e); } smt::Expression SMTChecker::var(Declaration const& _decl) { - solAssert(m_Variables.count(&_decl), ""); - return m_Variables.at(&_decl); + solAssert(m_variables.count(&_decl), ""); + return m_variables.at(&_decl); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index d23fd201..faaac639 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -103,8 +103,8 @@ private: std::shared_ptr<smt::SolverInterface> m_interface; std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_nextFreeSequenceCounter; - std::map<Expression const*, smt::Expression> m_Expressions; - std::map<Declaration const*, smt::Expression> m_Variables; + std::map<Expression const*, smt::Expression> m_expressions; + std::map<Declaration const*, smt::Expression> m_variables; ErrorReporter& m_errorReporter; FunctionDefinition const* m_currentFunction = nullptr; |