cerc-io/solidity
10
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 #10078 from blishko/chc_division_by_zero

Browse Source 
[SMTChecker] Enable division by zero checks in CHC engine
This commit is contained in:
Leonardo 2020-10-21 17:29:08 +01:00 committed by GitHub
commit dae41b4cfd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
16 changed files with 126 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -1,5 +1,7 @@
### 0.7.5 (unreleased) ### 0.7.5 (unreleased)
Compiler Features:
* SMTChecker: Add division by zero checks in the CHC engine.
Bugfixes: Bugfixes:
* SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.

7
libsolidity/formal/BMC.cpp
View File

@ -716,6 +716,13 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
void BMC::checkDivByZero(BMCVerificationTarget& _target) void BMC::checkDivByZero(BMCVerificationTarget& _target)
{ {
solAssert(_target.type == VerificationTarget::Type::DivByZero, ""); solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
if (
m_solvedTargets.count(_target.expression) &&
m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::DivByZero)
)
return;
checkCondition( checkCondition(
_target.constraints && (_target.value == 0), _target.constraints && (_target.value == 0),
_target.callStack, _target.callStack,

205
libsolidity/formal/CHC.cpp
View File

@ -533,18 +533,9 @@ void CHC::visitAssert(FunctionCall const& _funCall)
void CHC::visitAddMulMod(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), ""); 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); SMTEncoder::visitAddMulMod(_funCall);
} }
@ -643,13 +634,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, ""); solAssert(symbArray, "");
auto previousError = errorFlag().currentValue(); addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
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);
} }
pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation( pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@ -660,6 +645,9 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
frontend::Expression const& _expression 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); auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
IntegerType const* intType = nullptr; IntegerType const* intType = nullptr;
@ -673,46 +661,19 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned())) if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned()))
return values; return values;
auto previousError = errorFlag().currentValue();
errorFlag().increaseIndex();
VerificationTarget::Type targetType;
unsigned errorId = newErrorId(_expression);
optional<smtutil::Expression> target;
if (_op == Token::Div) if (_op == Token::Div)
{ addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
targetType = VerificationTarget::Type::Overflow;
target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
}
else if (intType->isSigned()) else if (intType->isSigned())
{ {
unsigned secondErrorId = newErrorId(_expression); addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
targetType = VerificationTarget::Type::UnderOverflow; addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
target = (values.second < intType->minValue() && errorFlag().currentValue() == errorId) ||
(values.second > intType->maxValue() && errorFlag().currentValue() == secondErrorId);
} }
else if (_op == Token::Sub) else if (_op == Token::Sub)
{ addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
targetType = VerificationTarget::Type::Underflow;
target = values.second < intType->minValue() && errorFlag().currentValue() == errorId;
}
else if (_op == Token::Add || _op == Token::Mul) else if (_op == Token::Add || _op == Token::Mul)
{ addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
targetType = VerificationTarget::Type::Overflow;
target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
}
else else
solAssert(false, ""); solAssert(false, "");
addVerificationTarget(
&_expression,
targetType,
errorFlag().currentValue()
);
m_context.addAssertion((errorFlag().currentValue() == previousError) || *target);
return values; return values;
} }
@ -1158,7 +1119,7 @@ void CHC::addVerificationTarget(
if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return; 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) 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) void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
{ {
addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
@ -1182,79 +1155,72 @@ void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression
void CHC::checkVerificationTargets() void CHC::checkVerificationTargets()
{ {
for (auto const& [scope, target]: m_verificationTargets) for (auto const& [scope, targets]: m_verificationTargets)
{ {
if (target.type == VerificationTarget::Type::Assert) for (size_t i = 0; i < targets.size(); ++i)
checkAssertTarget(scope, target);
else
{ {
string satMsg; auto const& target = targets[i];
string satMsgUnderflow;
string satMsgOverflow;
string unknownMsg;
ErrorId errorReporterId;
ErrorId underflowErrorId = 3944_error;
ErrorId overflowErrorId = 4984_error;
if (target.type == VerificationTarget::Type::PopEmptyArray) if (target.type == VerificationTarget::Type::Assert)
{ checkAssertTarget(scope, target);
solAssert(dynamic_cast<FunctionCall const*>(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<Expression const*>(scope);
solAssert(expr, "");
auto const* intType = dynamic_cast<IntegerType const*>(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);
else else
{ {
auto specificTarget = target; string satMsg;
specificTarget.type = VerificationTarget::Type::Underflow; string satMsgUnderflow;
checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow + " happens here.", satMsgUnderflow + " might happen here."); string satMsgOverflow;
string unknownMsg;
ErrorId errorReporterId;
ErrorId underflowErrorId = 3944_error;
ErrorId overflowErrorId = 4984_error;
++it; if (target.type == VerificationTarget::Type::PopEmptyArray)
{
solAssert(dynamic_cast<FunctionCall const*>(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<Expression const*>(scope);
solAssert(expr, "");
auto const* intType = dynamic_cast<IntegerType const*>(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(), ""); solAssert(it != m_errorIds.end(), "");
specificTarget.type = VerificationTarget::Type::Overflow; solAssert(i < it->second.size(), "");
checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow + " happens here.", satMsgOverflow + " might happen here."); 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()); auto it = m_errorIds.find(assertion->id());
solAssert(it != m_errorIds.end(), ""); 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."); 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. // because error id zero actually means no error in the CHC encoding.
if (errorId == 0) if (errorId == 0)
errorId = m_context.newUniqueId(); errorId = m_context.newUniqueId();
m_errorIds.emplace(_expr.id(), errorId); m_errorIds[_expr.id()].push_back(errorId);
return errorId; return errorId;
} }

10
libsolidity/formal/CHC.h
View File

@ -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 _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, 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 addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
void checkVerificationTargets(); void checkVerificationTargets();
@ -277,7 +278,9 @@ private:
smtutil::Expression errorId; smtutil::Expression errorId;
}; };
std::map<ASTNode const*, CHCVerificationTarget, IdCompare> 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<ASTNode const*, std::vector<CHCVerificationTarget>, IdCompare> m_verificationTargets;
/// Targets proven safe. /// Targets proven safe.
std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets; std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
@ -294,9 +297,8 @@ private:
std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions; std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
/// Maps ASTNode ids to error ids. /// Maps ASTNode ids to error ids.
/// A multimap is used instead of map anticipating the UnderOverflow /// There can be multiple errorIds associated with a single ASTNode.
/// target which has 2 error ids. std::map<unsigned, std::vector<unsigned>> m_errorIds;
std::multimap<unsigned, unsigned> m_errorIds;
/// The current block. /// The current block.
smtutil::Expression m_currentBlock = smtutil::Expression(true); smtutil::Expression m_currentBlock = smtutil::Expression(true);

13
libsolidity/formal/SMTEncoder.cpp
View File

@ -787,7 +787,6 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
auto x = expr(*args.at(0)); auto x = expr(*args.at(0));
auto y = expr(*args.at(1)); auto y = expr(*args.at(1));
auto k = expr(*args.at(2)); auto k = expr(*args.at(2));
m_context.addAssertion(k != 0);
auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type); auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
if (kind == FunctionType::Kind::AddMod) if (kind == FunctionType::Kind::AddMod)
@ -1532,8 +1531,6 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
if (_op == Token::Div || _op == Token::Mod) if (_op == Token::Div || _op == Token::Mod)
{ {
m_context.addAssertion(_right != 0);
// mod and unsigned division never underflow/overflow // mod and unsigned division never underflow/overflow
if (_op == Token::Mod || !intType->isSigned()) if (_op == Token::Mod || !intType->isSigned())
return {valueUnbounded, valueUnbounded}; return {valueUnbounded, valueUnbounded};
@ -1744,13 +1741,15 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left); m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
if (_type.isSigned()) if (_type.isSigned())
m_context.addAssertion( m_context.addAssertion(
(_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) || (_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) ||
(_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0) (_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0))
); );
else // unsigned version 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( void SMTEncoder::assignment(

4
scripts/error_codes.py
View File

@ -222,10 +222,10 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
old_source_only_ids = { old_source_only_ids = {
"1123", "1133", "1218", "1220", "1584", "1823", "1950", "1123", "1133", "1218", "1220", "1584", "1823", "1950",
"1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856", "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", "3893", "4010", "4281", "4802", "4805", "4828",
"4904", "4990", "5052", "5073", "5170", "5188", "5272", "5347", "5473", "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", "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140",
"8261", "8312", "8592", "8758", "9011", "8261", "8312", "8592", "8758", "9011",
"9085", "9390", "9440", "9547", "9551", "9615", "9980" "9085", "9390", "9440", "9547", "9551", "9615", "9980"

5
test/libsolidity/smtCheckerTests/math/addmod_1.sol
View File

@ -12,5 +12,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 3046: (141-166): BMC: Division by zero happens here. // Warning 4281: (141-166): CHC: Division by zero happens here.
// Warning 3046: (263-278): BMC: Division by zero happens here. // Warning 6328: (170-184): CHC: Assertion violation happens here.
// Warning 4281: (263-278): CHC: Division by zero happens here.

6
test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol
View File

@ -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 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 4281: (94-109): CHC: Division by zero happens here.
// Warning 3046: (180-195): BMC: 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.

5
test/libsolidity/smtCheckerTests/math/mulmod_1.sol
View File

@ -12,5 +12,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 3046: (141-166): BMC: Division by zero happens here. // Warning 4281: (141-166): CHC: Division by zero happens here.
// Warning 3046: (263-278): BMC: Division by zero happens here. // Warning 6328: (170-184): CHC: Assertion violation happens here.
// Warning 4281: (263-278): CHC: Division by zero happens here.

2
test/libsolidity/smtCheckerTests/operators/div_zero.sol
View File

@ -5,4 +5,4 @@ contract C {
uint x = 2 / z; uint x = 2 / z;
} }
// ---- // ----
// Warning 6084: (69-74): BMC: Division by zero happens here. // Warning 4281: (69-74): CHC: Division by zero happens here.

2
test/libsolidity/smtCheckerTests/operators/division_1.sol
View File

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

2
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
View File

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

2
test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol
View File

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

2
test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol
View File

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

2
test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol
View File

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

2
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
View File

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