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

Merge pull request #10652 from ethereum/smt_constants_inplce

Browse Source 
[SMTChecker] Replace constants by their value in-place
This commit is contained in:
Alex Beregszaszi 2020-12-18 14:22:32 +00:00 committed by GitHub
commit 7e20a095a8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 37 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
libsolidity/formal/SMTEncoder.cpp
View File

@ -932,7 +932,26 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
void SMTEncoder::endVisit(Identifier const& _identifier)
{
if (auto decl = identifierToVariable(_identifier))
{
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")

17
test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol Normal file
View File

@ -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.