aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-09-28 17:29:04 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2017-10-18 01:29:53 +0800
commit1f97c1ea8fec9a755d767811731f57fd527747b5 (patch)
tree064601c3395fdadef118968950b42a5dd3d3fe20 /libsolidity/formal
parent846b43479dc2991fbbab8b497a622fd58204e08e (diff)
downloaddexon-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.cpp18
-rw-r--r--libsolidity/formal/SMTChecker.h4
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;