mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Replace constants by their value in-place
This commit is contained in:
parent
6b482d4b41
commit
034d1ab90f
@ -932,7 +932,26 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
|
||||
void SMTEncoder::endVisit(Identifier const& _identifier)
|
||||
{
|
||||
if (auto decl = identifierToVariable(_identifier))
|
||||
defineExpr(_identifier, currentValue(*decl));
|
||||
{
|
||||
if (decl->isConstant())
|
||||
{
|
||||
if (RationalNumberType const* rationalType = isConstant(_identifier))
|
||||
{
|
||||
if (rationalType->isNegative())
|
||||
defineExpr(_identifier, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
|
||||
else
|
||||
defineExpr(_identifier, smtutil::Expression(rationalType->literalValue(nullptr)));
|
||||
}
|
||||
else
|
||||
{
|
||||
solAssert(decl->value(), "");
|
||||
decl->value()->accept(*this);
|
||||
defineExpr(_identifier, expr(*decl->value()));
|
||||
}
|
||||
}
|
||||
else
|
||||
defineExpr(_identifier, currentValue(*decl));
|
||||
}
|
||||
else if (_identifier.annotation().type->category() == Type::Category::Function)
|
||||
visitFunctionIdentifier(_identifier);
|
||||
else if (_identifier.name() == "now")
|
||||
|
@ -0,0 +1,17 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract DepositContract {
|
||||
uint constant MAX_DEPOSIT_COUNT = 2**32 - 1;
|
||||
|
||||
uint256 deposit_count;
|
||||
uint256 deposit_count_2;
|
||||
|
||||
function deposit() external {
|
||||
require(deposit_count < MAX_DEPOSIT_COUNT);
|
||||
deposit_count += 1;
|
||||
deposit_count_2 += 10; // should fail
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 4984: (289-310): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
|
||||
// Warning 2661: (289-310): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
|
Loading…
Reference in New Issue
Block a user