cerc-io/solidity
11
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] Refactor setZeroValue and setUnknownValue

Browse Source
This commit is contained in:
Leonardo Alt
2018-11-22 16:42:51 +01:00
parent be321090e6
commit ec84a7dc9b
6 changed files with 58 additions and 44 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SymbolicVariables.cpp
-22
View File
@@ -62,15 +62,6 @@ smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
}
void SymbolicBoolVariable::setZeroValue()
{
m_interface.addAssertion(currentValue() == smt::Expression(false));
}
void SymbolicBoolVariable::setUnknownValue()
{
}
SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type,
string const& _uniqueName,
@@ -86,19 +77,6 @@ smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
}
void SymbolicIntVariable::setZeroValue()
{
m_interface.addAssertion(currentValue() == 0);
}
void SymbolicIntVariable::setUnknownValue()
{
auto intType = dynamic_cast<IntegerType const*>(m_type.get());
solAssert(intType, "");
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}
SymbolicAddressVariable::SymbolicAddressVariable(
string const& _uniqueName,
smt::SolverInterface& _interface