cerc-io/solidity
15
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

Fix possibly effectless map emplace

Browse Source
This commit is contained in:
Leonardo Alt 2018-10-17 19:00:38 +02:00
parent c92d3b537d
commit 070471d8d4
1 changed files with 10 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/formal/SMTChecker.cpp
View File

@ -992,6 +992,8 @@ void SMTChecker::createExpr(Expression const& _e)
solAssert(_e.annotation().type, ""); solAssert(_e.annotation().type, "");
if (hasExpr(_e)) if (hasExpr(_e))
m_expressions.at(&_e)->increaseIndex(); m_expressions.at(&_e)->increaseIndex();
else
{
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
m_expressions.emplace(&_e, result.second); m_expressions.emplace(&_e, result.second);
if (result.first) if (result.first)
@ -999,6 +1001,7 @@ void SMTChecker::createExpr(Expression const& _e)
_e.location(), _e.location(),
"Assertion checker does not yet implement this type." "Assertion checker does not yet implement this type."
); );
}
} }
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)