From f0d81601db495e6d2f23f41381e2e7a480837639 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 19 Oct 2020 18:54:42 +0200 Subject: [PATCH] [SMTChecker] Adding division by zero checks in the CHC engine --- Changelog.md | 2 + libsolidity/formal/BMC.cpp | 7 + libsolidity/formal/CHC.cpp | 205 ++++++++---------- libsolidity/formal/CHC.h | 10 +- libsolidity/formal/SMTEncoder.cpp | 13 +- scripts/error_codes.py | 4 +- .../smtCheckerTests/math/addmod_1.sol | 5 +- .../math/addmod_mulmod_zero.sol | 6 +- .../smtCheckerTests/math/mulmod_1.sol | 5 +- .../smtCheckerTests/operators/div_zero.sol | 2 +- .../smtCheckerTests/operators/division_1.sol | 2 +- .../overflow/signed_div_overflow.sol | 2 +- .../overflow/signed_mod_overflow.sol | 2 +- .../overflow/unsigned_div_overflow.sol | 2 +- .../overflow/unsigned_mod_overflow.sol | 2 +- .../types/fixed_bytes_access_2.sol | 2 +- 16 files changed, 126 insertions(+), 145 deletions(-) diff --git a/Changelog.md b/Changelog.md index fee4eb648..f02123341 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,7 @@ ### 0.7.5 (unreleased) +Compiler Features: + * SMTChecker: Add division by zero checks in the CHC engine. Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dc1a08472..e41c69cd2 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -716,6 +716,13 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons void BMC::checkDivByZero(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::DivByZero, ""); + + if ( + m_solvedTargets.count(_target.expression) && + m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::DivByZero) + ) + return; + checkCondition( _target.constraints && (_target.value == 0), _target.callStack, diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 880e9c553..7bedc8a65 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -533,18 +533,9 @@ void CHC::visitAssert(FunctionCall const& _funCall) void CHC::visitAddMulMod(FunctionCall const& _funCall) { - auto previousError = errorFlag().currentValue(); - errorFlag().increaseIndex(); - - addVerificationTarget( - &_funCall, - VerificationTarget::Type::DivByZero, - errorFlag().currentValue() - ); - solAssert(_funCall.arguments().at(2), ""); - smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall); - m_context.addAssertion((errorFlag().currentValue() == previousError) || target); + + addVerificationTarget(_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0); SMTEncoder::visitAddMulMod(_funCall); } @@ -643,13 +634,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); - auto previousError = errorFlag().currentValue(); - errorFlag().increaseIndex(); - - addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, errorFlag().currentValue()); - - smtutil::Expression target = (symbArray->length() <= 0) && (errorFlag().currentValue() == newErrorId(_arrayPop)); - m_context.addAssertion((errorFlag().currentValue() == previousError) || target); + addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0); } pair CHC::arithmeticOperation( @@ -660,6 +645,9 @@ pair CHC::arithmeticOperation( frontend::Expression const& _expression ) { + if (_op == Token::Mod || _op == Token::Div) + addVerificationTarget(_expression, VerificationTarget::Type::DivByZero, _right == 0); + auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression); IntegerType const* intType = nullptr; @@ -673,46 +661,19 @@ pair CHC::arithmeticOperation( if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned())) return values; - auto previousError = errorFlag().currentValue(); - errorFlag().increaseIndex(); - - VerificationTarget::Type targetType; - unsigned errorId = newErrorId(_expression); - - optional target; if (_op == Token::Div) - { - targetType = VerificationTarget::Type::Overflow; - target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId; - } + addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue()); else if (intType->isSigned()) { - unsigned secondErrorId = newErrorId(_expression); - targetType = VerificationTarget::Type::UnderOverflow; - target = (values.second < intType->minValue() && errorFlag().currentValue() == errorId) || - (values.second > intType->maxValue() && errorFlag().currentValue() == secondErrorId); + addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue()); + addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue()); } else if (_op == Token::Sub) - { - targetType = VerificationTarget::Type::Underflow; - target = values.second < intType->minValue() && errorFlag().currentValue() == errorId; - } + addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue()); else if (_op == Token::Add || _op == Token::Mul) - { - targetType = VerificationTarget::Type::Overflow; - target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId; - } + addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue()); else solAssert(false, ""); - - addVerificationTarget( - &_expression, - targetType, - errorFlag().currentValue() - ); - - m_context.addAssertion((errorFlag().currentValue() == previousError) || *target); - return values; } @@ -1158,7 +1119,7 @@ void CHC::addVerificationTarget( if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) return; - m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); + m_verificationTargets[_scope].push_back(CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); } void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId) @@ -1175,6 +1136,18 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type } } +void CHC::addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target) +{ + auto previousError = errorFlag().currentValue(); + errorFlag().increaseIndex(); + addVerificationTarget(&_scope, _type, errorFlag().currentValue()); + + m_context.addAssertion( + errorFlag().currentValue() == previousError || + (_target && errorFlag().currentValue() == newErrorId(_scope)) + ); +} + void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId) { addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); @@ -1182,79 +1155,72 @@ void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression void CHC::checkVerificationTargets() { - for (auto const& [scope, target]: m_verificationTargets) + for (auto const& [scope, targets]: m_verificationTargets) { - if (target.type == VerificationTarget::Type::Assert) - checkAssertTarget(scope, target); - else + for (size_t i = 0; i < targets.size(); ++i) { - string satMsg; - string satMsgUnderflow; - string satMsgOverflow; - string unknownMsg; - ErrorId errorReporterId; - ErrorId underflowErrorId = 3944_error; - ErrorId overflowErrorId = 4984_error; + auto const& target = targets[i]; - if (target.type == VerificationTarget::Type::PopEmptyArray) - { - solAssert(dynamic_cast(scope), ""); - satMsg = "Empty array \"pop\" detected here."; - unknownMsg = "Empty array \"pop\" might happen here."; - errorReporterId = 2529_error; - } - else if ( - target.type == VerificationTarget::Type::Underflow || - target.type == VerificationTarget::Type::Overflow || - target.type == VerificationTarget::Type::UnderOverflow - ) - { - auto const* expr = dynamic_cast(scope); - solAssert(expr, ""); - auto const* intType = dynamic_cast(expr->annotation().type); - if (!intType) - intType = TypeProvider::uint256(); - - satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")"; - satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")"; - if (target.type == VerificationTarget::Type::Underflow) - { - satMsg = satMsgUnderflow + " happens here."; - unknownMsg = satMsgUnderflow + " might happen here."; - errorReporterId = underflowErrorId; - } - else if (target.type == VerificationTarget::Type::Overflow) - { - satMsg = satMsgOverflow + " happens here."; - unknownMsg = satMsgOverflow + " might happen here."; - errorReporterId = overflowErrorId; - } - } - else if (target.type == VerificationTarget::Type::DivByZero) - { - satMsg = "Division by zero happens here."; - unknownMsg = "Division by zero might happen here."; - errorReporterId = 4281_error; - } - else - solAssert(false, ""); - - auto it = m_errorIds.find(scope->id()); - solAssert(it != m_errorIds.end(), ""); - unsigned errorId = it->second; - - if (target.type != VerificationTarget::Type::UnderOverflow) - checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg); + if (target.type == VerificationTarget::Type::Assert) + checkAssertTarget(scope, target); else { - auto specificTarget = target; - specificTarget.type = VerificationTarget::Type::Underflow; - checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow + " happens here.", satMsgUnderflow + " might happen here."); + string satMsg; + string satMsgUnderflow; + string satMsgOverflow; + string unknownMsg; + ErrorId errorReporterId; + ErrorId underflowErrorId = 3944_error; + ErrorId overflowErrorId = 4984_error; - ++it; + if (target.type == VerificationTarget::Type::PopEmptyArray) + { + solAssert(dynamic_cast(scope), ""); + satMsg = "Empty array \"pop\" detected here."; + unknownMsg = "Empty array \"pop\" might happen here."; + errorReporterId = 2529_error; + } + else if ( + target.type == VerificationTarget::Type::Underflow || + target.type == VerificationTarget::Type::Overflow + ) + { + auto const* expr = dynamic_cast(scope); + solAssert(expr, ""); + auto const* intType = dynamic_cast(expr->annotation().type); + if (!intType) + intType = TypeProvider::uint256(); + + satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")"; + satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")"; + if (target.type == VerificationTarget::Type::Underflow) + { + satMsg = satMsgUnderflow + " happens here."; + unknownMsg = satMsgUnderflow + " might happen here."; + errorReporterId = underflowErrorId; + } + else if (target.type == VerificationTarget::Type::Overflow) + { + satMsg = satMsgOverflow + " happens here."; + unknownMsg = satMsgOverflow + " might happen here."; + errorReporterId = overflowErrorId; + } + } + else if (target.type == VerificationTarget::Type::DivByZero) + { + satMsg = "Division by zero happens here."; + unknownMsg = "Division by zero might happen here."; + errorReporterId = 4281_error; + } + else + solAssert(false, ""); + + auto it = m_errorIds.find(scope->id()); solAssert(it != m_errorIds.end(), ""); - specificTarget.type = VerificationTarget::Type::Overflow; - checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow + " happens here.", satMsgOverflow + " might happen here."); + solAssert(i < it->second.size(), ""); + unsigned errorId = it->second[i]; + + checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg); } } } @@ -1268,7 +1234,8 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& { auto it = m_errorIds.find(assertion->id()); solAssert(it != m_errorIds.end(), ""); - unsigned errorId = it->second; + solAssert(!it->second.empty(), ""); + unsigned errorId = it->second[0]; checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here."); } @@ -1464,7 +1431,7 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr) // because error id zero actually means no error in the CHC encoding. if (errorId == 0) errorId = m_context.newUniqueId(); - m_errorIds.emplace(_expr.id(), errorId); + m_errorIds[_expr.id()].push_back(errorId); return errorId; } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index b47043781..0bae37084 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -183,6 +183,7 @@ private: void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId); + void addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target); void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); void checkVerificationTargets(); @@ -277,7 +278,9 @@ private: smtutil::Expression errorId; }; - std::map m_verificationTargets; + /// Verification targets corresponding to ASTNodes. There can be multiple targets for a single ASTNode, + /// e.g., divByZero and Overflow for signed division. + std::map, IdCompare> m_verificationTargets; /// Targets proven safe. std::map> m_safeTargets; @@ -294,9 +297,8 @@ private: std::map, IdCompare> m_functionAssertions; /// Maps ASTNode ids to error ids. - /// A multimap is used instead of map anticipating the UnderOverflow - /// target which has 2 error ids. - std::multimap m_errorIds; + /// There can be multiple errorIds associated with a single ASTNode. + std::map> m_errorIds; /// The current block. smtutil::Expression m_currentBlock = smtutil::Expression(true); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 9092e417c..c114b75be 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -787,7 +787,6 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall) auto x = expr(*args.at(0)); auto y = expr(*args.at(1)); auto k = expr(*args.at(2)); - m_context.addAssertion(k != 0); auto const& intType = dynamic_cast(*_funCall.annotation().type); if (kind == FunctionType::Kind::AddMod) @@ -1532,8 +1531,6 @@ pair SMTEncoder::arithmeticOperation( if (_op == Token::Div || _op == Token::Mod) { - m_context.addAssertion(_right != 0); - // mod and unsigned division never underflow/overflow if (_op == Token::Mod || !intType->isSigned()) return {valueUnbounded, valueUnbounded}; @@ -1744,13 +1741,15 @@ pair SMTEncoder::divModWithSlacks( m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left); if (_type.isSigned()) m_context.addAssertion( - (_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) || - (_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0) + (_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) || + (_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0)) ); else // unsigned version - m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right); + m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right)); - return {d.currentValue(), r.currentValue()}; + auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue()); + auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue()); + return {divResult, modResult}; } void SMTEncoder::assignment( diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 100c0c0be..ad0374a76 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -222,10 +222,10 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): old_source_only_ids = { "1123", "1133", "1218", "1220", "1584", "1823", "1950", "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856", - "3263", "3356", "3441", "3682", "3876", + "3046", "3263", "3356", "3441", "3682", "3876", "3893", "4010", "4281", "4802", "4805", "4828", "4904", "4990", "5052", "5073", "5170", "5188", "5272", "5347", "5473", - "5622", "6041", "6052", "6272", "6708", "6792", "6931", "7110", "7128", "7186", + "5622", "6041", "6052", "6084", "6272", "6708", "6792", "6931", "7110", "7128", "7186", "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140", "8261", "8312", "8592", "8758", "9011", "9085", "9390", "9440", "9547", "9551", "9615", "9980" diff --git a/test/libsolidity/smtCheckerTests/math/addmod_1.sol b/test/libsolidity/smtCheckerTests/math/addmod_1.sol index a4ebed099..ae669c90d 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_1.sol @@ -12,5 +12,6 @@ contract C { } } // ---- -// Warning 3046: (141-166): BMC: Division by zero happens here. -// Warning 3046: (263-278): BMC: Division by zero happens here. +// Warning 4281: (141-166): CHC: Division by zero happens here. +// Warning 6328: (170-184): CHC: Assertion violation happens here. +// Warning 4281: (263-278): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol index 84c6e4698..1d73d60f4 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol @@ -22,5 +22,7 @@ contract C { } // ---- // Warning 6321: (253-260): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 3046: (94-109): BMC: Division by zero happens here. -// Warning 3046: (180-195): BMC: Division by zero happens here. +// Warning 4281: (94-109): CHC: Division by zero happens here. +// Warning 6328: (113-126): CHC: Assertion violation happens here. +// Warning 4281: (180-195): CHC: Division by zero happens here. +// Warning 6328: (199-212): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol index d75e6d267..ce9efdce5 100644 --- a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol @@ -12,5 +12,6 @@ contract C { } } // ---- -// Warning 3046: (141-166): BMC: Division by zero happens here. -// Warning 3046: (263-278): BMC: Division by zero happens here. +// Warning 4281: (141-166): CHC: Division by zero happens here. +// Warning 6328: (170-184): CHC: Assertion violation happens here. +// Warning 4281: (263-278): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/div_zero.sol b/test/libsolidity/smtCheckerTests/operators/div_zero.sol index b11b82d0e..b6fb4ed19 100644 --- a/test/libsolidity/smtCheckerTests/operators/div_zero.sol +++ b/test/libsolidity/smtCheckerTests/operators/div_zero.sol @@ -5,4 +5,4 @@ contract C { uint x = 2 / z; } // ---- -// Warning 6084: (69-74): BMC: Division by zero happens here. +// Warning 4281: (69-74): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/division_1.sol b/test/libsolidity/smtCheckerTests/operators/division_1.sol index 99b36e480..87455a4e5 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_1.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// Warning 3046: (111-116): BMC: Division by zero happens here. +// Warning 4281: (111-116): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol index a3ef63779..77d9a4847 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol @@ -6,5 +6,5 @@ contract C { } } // ---- +// Warning 4281: (110-115): CHC: Division by zero happens here. // Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. -// Warning 3046: (110-115): BMC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol index df275044b..7cb939586 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 3046: (110-115): BMC: Division by zero happens here. +// Warning 4281: (110-115): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol index e8a5dc76a..7005fd1b5 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 3046: (113-118): BMC: Division by zero happens here. +// Warning 4281: (113-118): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol index 59bb034c5..3019baa6f 100644 --- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 3046: (113-118): BMC: Division by zero happens here. +// Warning 4281: (113-118): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol index ea645ccaf..add65c141 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 3046: (117-120): BMC: Division by zero happens here. +// Warning 4281: (117-120): CHC: Division by zero happens here.