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 #9770 from ethereum/smt_dot

Browse Source 
[SMTChecker] Change warning message
This commit is contained in:
chriseth 2020-09-09 17:17:04 +02:00 committed by GitHub
commit c966971fd3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
334 changed files with 547 additions and 550 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/BMC.cpp
View File

@ -836,11 +836,11 @@ void BMC::checkCondition(
case smtutil::CheckResult::SATISFIABLE: case smtutil::CheckResult::SATISFIABLE:
{ {
std::ostringstream message; std::ostringstream message;
message << _description << " happens here"; message << _description << " happens here.";
if (_callStack.size()) if (_callStack.size())
{ {
std::ostringstream modelMessage; std::ostringstream modelMessage;
modelMessage << " for:\n"; modelMessage << "\nCounterexample:\n";
solAssert(values.size() == expressionNames.size(), ""); solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel; map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i) for (size_t i = 0; i < values.size(); ++i)
@ -859,10 +859,7 @@ void BMC::checkCondition(
); );
} }
else else
{
message << ".";
m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation); m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation);
}
break; break;
} }
case smtutil::CheckResult::UNSATISFIABLE: case smtutil::CheckResult::UNSATISFIABLE:

12
libsolidity/formal/CHC.cpp
View File

@ -1251,7 +1251,7 @@ void CHC::checkVerificationTargets()
if (target.type == VerificationTarget::Type::PopEmptyArray) if (target.type == VerificationTarget::Type::PopEmptyArray)
{ {
solAssert(dynamic_cast<FunctionCall const*>(scope), ""); solAssert(dynamic_cast<FunctionCall const*>(scope), "");
satMsg = "Empty array \"pop\" detected here"; satMsg = "Empty array \"pop\" detected here.";
unknownMsg = "Empty array \"pop\" might happen here."; unknownMsg = "Empty array \"pop\" might happen here.";
errorReporterId = 2529_error; errorReporterId = 2529_error;
} }
@ -1267,8 +1267,8 @@ void CHC::checkVerificationTargets()
if (!intType) if (!intType)
intType = TypeProvider::uint256(); intType = TypeProvider::uint256();
satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here"; satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here.";
satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here"; satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here.";
if (target.type == VerificationTarget::Type::Underflow) if (target.type == VerificationTarget::Type::Underflow)
{ {
satMsg = satMsgUnderflow; satMsg = satMsgUnderflow;
@ -1314,7 +1314,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
solAssert(it != m_errorIds.end(), ""); solAssert(it != m_errorIds.end(), "");
unsigned errorId = it->second; unsigned errorId = it->second;
checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here"); checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.");
} }
} }
@ -1345,13 +1345,13 @@ void CHC::checkAndReportTarget(
_errorReporterId, _errorReporterId,
_scope->location(), _scope->location(),
_satMsg, _satMsg,
SecondarySourceLocation().append(" for:\n" + *cex, SourceLocation{}) SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{})
); );
else else
m_outerErrorReporter.warning( m_outerErrorReporter.warning(
_errorReporterId, _errorReporterId,
_scope->location(), _scope->location(),
_satMsg + "." _satMsg
); );
} }
else if (!_unknownMsg.empty()) else if (!_unknownMsg.empty())

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol
View File

@ -8,4 +8,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (82-89): Empty array "pop" detected here // Warning 2529: (82-89): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol
View File

@ -8,4 +8,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (82-89): Empty array "pop" detected here // Warning 2529: (82-89): Empty array "pop" detected here.

4
test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol
View File

@ -8,5 +8,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (82-89): Empty array "pop" detected here // Warning 2529: (82-89): Empty array "pop" detected here.
// Warning 2529: (93-100): Empty array "pop" detected here // Warning 2529: (93-100): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol
View File

@ -8,4 +8,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (94-101): Empty array "pop" detected here // Warning 2529: (94-101): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol
View File

@ -11,4 +11,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (122-129): Empty array "pop" detected here // Warning 2529: (122-129): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol
View File

@ -11,4 +11,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (127-134): Empty array "pop" detected here // Warning 2529: (127-134): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol
View File

@ -13,4 +13,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (82-89): Empty array "pop" detected here // Warning 2529: (82-89): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/length_basic.sol
View File

@ -10,4 +10,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (153-176): Assertion violation happens here // Warning 6328: (153-176): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
View File

@ -14,6 +14,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (198-224): Assertion violation happens here // Warning 6328: (198-224): Assertion violation happens here.
// Warning 6328: (228-254): Assertion violation happens here // Warning 6328: (228-254): Assertion violation happens here.
// Warning 6328: (258-281): Assertion violation happens here // Warning 6328: (258-281): Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -16,7 +16,7 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (222-248): Assertion violation happens here // Warning 6328: (222-248): Assertion violation happens here.
// Warning 6328: (252-278): Assertion violation happens here // Warning 6328: (252-278): Assertion violation happens here.
// Warning 6328: (282-305): Assertion violation happens here // Warning 6328: (282-305): Assertion violation happens here.
// Warning 6328: (309-335): Assertion violation happens here // Warning 6328: (309-335): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
View File

@ -7,4 +7,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (82-89): Empty array "pop" detected here // Warning 2529: (82-89): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (111-121): Empty array "pop" detected here // Warning 2529: (111-121): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
View File

@ -7,4 +7,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (76-83): Empty array "pop" detected here // Warning 2529: (76-83): Empty array "pop" detected here.

2
test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
View File

@ -11,4 +11,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 2529: (150-157): Empty array "pop" detected here // Warning 2529: (150-157): Empty array "pop" detected here.

4
test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
View File

@ -10,5 +10,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 3944: (162-177): Underflow (resulting value less than 0) happens here // Warning 3944: (162-177): Underflow (resulting value less than 0) happens here.
// Warning 6328: (150-184): Assertion violation happens here // Warning 6328: (150-184): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol
View File

@ -8,5 +8,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (113-139): Assertion violation happens here // Warning 6328: (113-139): Assertion violation happens here.
// Warning 6328: (143-189): Assertion violation happens here // Warning 6328: (143-189): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
View File

@ -10,6 +10,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (122-148): Assertion violation happens here // Warning 6328: (122-148): Assertion violation happens here.
// Warning 6328: (202-218): Assertion violation happens here // Warning 6328: (202-218): Assertion violation happens here.
// Warning 6328: (222-278): Assertion violation happens here // Warning 6328: (222-278): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
View File

@ -12,5 +12,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 3944: (217-232): Underflow (resulting value less than 0) happens here // Warning 3944: (217-232): Underflow (resulting value less than 0) happens here.
// Warning 6328: (205-239): Assertion violation happens here // Warning 6328: (205-239): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -12,4 +12,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (167-188): Assertion violation happens here // Warning 6328: (167-188): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -18,6 +18,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (193-217): Assertion violation happens here // Warning 6328: (193-217): Assertion violation happens here.
// Warning 6328: (309-333): Assertion violation happens here // Warning 6328: (309-333): Assertion violation happens here.
// Warning 6328: (419-436): Assertion violation happens here // Warning 6328: (419-436): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (111-144): Assertion violation happens here // Warning 6328: (111-144): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
View File

@ -8,4 +8,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (94-124): Assertion violation happens here // Warning 6328: (94-124): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
View File

@ -15,4 +15,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (184-213): Assertion violation happens here // Warning 6328: (184-213): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
View File

@ -53,4 +53,4 @@ contract MyConc{
// ---- // ----
// Warning 2519: (773-792): This declaration shadows an existing declaration. // Warning 2519: (773-792): This declaration shadows an existing declaration.
// Warning 2018: (1009-1086): Function state mutability can be restricted to view // Warning 2018: (1009-1086): Function state mutability can be restricted to view
// Warning 4984: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
View File

@ -15,4 +15,4 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (227-236): Assertion violation happens here // Warning 6328: (227-236): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
View File

@ -17,5 +17,5 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (202-218): Assertion violation happens here // Warning 6328: (202-218): Assertion violation happens here.
// Warning 6328: (242-252): Assertion violation happens here // Warning 6328: (242-252): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
View File

@ -15,4 +15,4 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (225-235): Assertion violation happens here // Warning 6328: (225-235): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
View File

@ -15,4 +15,4 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (225-235): Assertion violation happens here // Warning 6328: (225-235): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
View File

@ -24,4 +24,4 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (360-370): Assertion violation happens here // Warning 6328: (360-370): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
View File

@ -15,4 +15,4 @@ contract c {
} }
} }
// ---- // ----
// Warning 6328: (225-235): Assertion violation happens here // Warning 6328: (225-235): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (159-173): Assertion violation happens here // Warning 6328: (159-173): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (159-173): Assertion violation happens here // Warning 6328: (159-173): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (161-175): Assertion violation happens here // Warning 6328: (161-175): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external.sol
View File

@ -17,4 +17,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (200-214): Assertion violation happens here // Warning 6328: (200-214): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash.sol
View File

@ -26,4 +26,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (423-445): Assertion violation happens here // Warning 6328: (423-445): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol
View File

@ -28,4 +28,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (431-453): Assertion violation happens here // Warning 6328: (431-453): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
View File

@ -34,5 +34,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (528-565): Assertion violation happens here // Warning 6328: (528-565): Assertion violation happens here.
// Warning 5084: (544-554): Type conversion is not yet fully supported and might yield false positives. // Warning 5084: (544-554): Type conversion is not yet fully supported and might yield false positives.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol
View File

@ -29,4 +29,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (299-313): Assertion violation happens here // Warning 6328: (299-313): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
View File

@ -42,6 +42,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (452-466): Assertion violation happens here // Warning 6328: (452-466): Assertion violation happens here.
// Warning 6328: (470-496): Assertion violation happens here // Warning 6328: (470-496): Assertion violation happens here.
// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives. // Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
View File

@ -34,6 +34,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (381-395): Assertion violation happens here // Warning 6328: (381-395): Assertion violation happens here.
// Warning 6328: (399-425): Assertion violation happens here // Warning 6328: (399-425): Assertion violation happens here.
// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives. // Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
View File

@ -38,6 +38,6 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (435-461): Assertion violation happens here // Warning 6328: (435-461): Assertion violation happens here.
// Warning 6328: (594-631): Assertion violation happens here // Warning 6328: (594-631): Assertion violation happens here.
// Warning 5084: (610-620): Type conversion is not yet fully supported and might yield false positives. // Warning 5084: (610-620): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -18,5 +18,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (189-203): Assertion violation happens here // Warning 6328: (189-203): Assertion violation happens here.
// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol
View File

@ -25,4 +25,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (286-303): Assertion violation happens here // Warning 6328: (286-303): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol
View File

@ -23,4 +23,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (256-273): Assertion violation happens here // Warning 6328: (256-273): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol
View File

@ -27,4 +27,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (307-321): Assertion violation happens here // Warning 6328: (307-321): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol
View File

@ -13,4 +13,4 @@ contract A is C {
} }
} }
// ---- // ----
// Warning 6328: (152-166): Assertion violation happens here // Warning 6328: (152-166): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol
View File

@ -4,4 +4,4 @@ contract A is C { constructor() C(2) { assert(a == 2); } }
contract B is C { constructor() C(3) { assert(a == 3); } } contract B is C { constructor() C(3) { assert(a == 3); } }
contract J is C { constructor() C(3) { assert(a == 4); } } contract J is C { constructor() C(3) { assert(a == 4); } }
// ---- // ----
// Warning 6328: (243-257): Assertion violation happens here // Warning 6328: (243-257): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
View File

@ -19,6 +19,6 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (232-250): Assertion violation happens here // Warning 6328: (232-250): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -18,6 +18,6 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 4984: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here.

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol
View File

@ -25,6 +25,6 @@ contract A is B2, B1 {
} }
} }
// ---- // ----
// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-320): Assertion violation happens here // Warning 6328: (302-320): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
View File

@ -25,6 +25,6 @@ contract A is B2, B1 {
} }
} }
// ---- // ----
// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-320): Assertion violation happens here // Warning 6328: (302-320): Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -27,7 +27,7 @@ contract A is B2, B1 {
} }
} }
// ---- // ----
// Warning 4984: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (334-350): Assertion violation happens here // Warning 6328: (334-350): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol
View File

@ -20,4 +20,4 @@ contract A is B, B2 {
} }
// ---- // ----
// Warning 5667: (164-170): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (164-170): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (194-208): Assertion violation happens here // Warning 6328: (194-208): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol
View File

@ -19,4 +19,4 @@ contract A is B {
} }
// ---- // ----
// Warning 5667: (194-200): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (194-200): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (224-238): Assertion violation happens here // Warning 6328: (224-238): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol
View File

@ -17,4 +17,4 @@ contract A is B {
} }
// ---- // ----
// Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (172-186): Assertion violation happens here // Warning 6328: (172-186): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol
View File

@ -16,4 +16,4 @@ contract A is B {
} }
// ---- // ----
// Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (150-164): Assertion violation happens here // Warning 6328: (150-164): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol
View File

@ -27,4 +27,4 @@ contract A is B {
} }
// ---- // ----
// Warning 5667: (254-260): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (254-260): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (284-298): Assertion violation happens here // Warning 6328: (284-298): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol
View File

@ -32,4 +32,4 @@ contract A is B {
} }
// ---- // ----
// Warning 5667: (296-302): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (296-302): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (357-372): Assertion violation happens here // Warning 6328: (357-372): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol
View File

@ -25,5 +25,5 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (328-342): Assertion violation happens here // Warning 6328: (328-342): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol
View File

@ -23,4 +23,4 @@ contract B is C {
contract A is B { contract A is B {
} }
// ---- // ----
// Warning 6328: (266-280): Assertion violation happens here // Warning 6328: (266-280): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol
View File

@ -14,4 +14,4 @@ contract A is C {
} }
} }
// ---- // ----
// Warning 6328: (188-202): Assertion violation happens here // Warning 6328: (188-202): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol
View File

@ -13,5 +13,5 @@ contract A is C {
} }
} }
// ---- // ----
// Warning 6328: (134-148): Assertion violation happens here // Warning 6328: (134-148): Assertion violation happens here.
// Warning 6328: (152-168): Assertion violation happens here // Warning 6328: (152-168): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_simple.sol
View File

@ -13,4 +13,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (141-155): Assertion violation happens here // Warning 6328: (141-155): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
View File

@ -13,4 +13,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (145-159): Assertion violation happens here // Warning 6328: (145-159): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
View File

@ -15,4 +15,4 @@ contract C is B {
} }
} }
// ---- // ----
// Warning 6328: (165-179): Assertion violation happens here // Warning 6328: (165-179): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -13,5 +13,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 4984: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (162-176): Assertion violation happens here // Warning 6328: (162-176): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol
View File

@ -9,4 +9,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (116-132): Assertion violation happens here // Warning 6328: (116-132): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol
View File

@ -16,4 +16,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (209-223): Assertion violation happens here // Warning 6328: (209-223): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol
View File

@ -24,5 +24,5 @@ contract C
} }
// ---- // ----
// Warning 6328: (209-223): Assertion violation happens here // Warning 6328: (209-223): Assertion violation happens here.
// Warning 6328: (321-335): Assertion violation happens here // Warning 6328: (321-335): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol
View File

@ -18,4 +18,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (261-277): Assertion violation happens here // Warning 6328: (261-277): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -17,4 +17,4 @@ contract C
} }
} }
// ---- // ----
// Warning 4661: (297-321): Assertion violation happens here // Warning 4661: (297-321): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_external_4.sol
View File

@ -16,4 +16,4 @@ contract D
} }
} }
// ---- // ----
// Warning 6328: (191-206): Assertion violation happens here // Warning 6328: (191-206): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
View File

@ -12,4 +12,4 @@ contract C
} }
// ---- // ----
// Warning 6328: (161-174): Assertion violation happens here // Warning 6328: (161-174): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
View File

@ -16,4 +16,4 @@ contract C
} }
// ---- // ----
// Warning 6328: (229-242): Assertion violation happens here // Warning 6328: (229-242): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
View File

@ -12,4 +12,4 @@ contract C
} }
// ---- // ----
// Warning 6328: (163-176): Assertion violation happens here // Warning 6328: (163-176): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
View File

@ -17,5 +17,5 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (245-261): Assertion violation happens here // Warning 6328: (245-261): Assertion violation happens here.
// Warning 8364: (228-229): Assertion checker does not yet implement type type(library L) // Warning 8364: (228-229): Assertion checker does not yet implement type type(library L)

2
test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
View File

@ -13,4 +13,4 @@ contract C
} }
// ---- // ----
// Warning 6328: (144-157): Assertion violation happens here // Warning 6328: (144-157): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
View File

@ -14,4 +14,4 @@ contract C
} }
// ---- // ----
// Warning 6328: (152-165): Assertion violation happens here // Warning 6328: (152-165): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol
View File

@ -17,4 +17,4 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 6328: (254-268): Assertion violation happens here // Warning 6328: (254-268): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol
View File

@ -21,4 +21,4 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 6328: (274-288): Assertion violation happens here // Warning 6328: (274-288): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol
View File

@ -21,5 +21,5 @@ contract C{
} }
// ---- // ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (238-241): Underflow (resulting value less than 0) happens here // Warning 4144: (238-241): Underflow (resulting value less than 0) happens here.

14
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
View File

@ -21,10 +21,10 @@ contract C{
} }
// ---- // ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (138-152): Assertion violation happens here // Warning 6328: (138-152): Assertion violation happens here.
// Warning 6328: (170-184): Assertion violation happens here // Warning 6328: (170-184): Assertion violation happens here.
// Warning 6328: (220-234): Assertion violation happens here // Warning 6328: (220-234): Assertion violation happens here.
// Warning 6328: (245-259): Assertion violation happens here // Warning 6328: (245-259): Assertion violation happens here.
// Warning 6328: (82-96): Assertion violation happens here // Warning 6328: (82-96): Assertion violation happens here.
// Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (238-241): Underflow (resulting value less than 0) happens here // Warning 4144: (238-241): Underflow (resulting value less than 0) happens here.

4
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol
View File

@ -17,5 +17,5 @@ contract C is A {
} }
} }
// ---- // ----
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here.
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here.

10
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol
View File

@ -17,8 +17,8 @@ contract C is A {
} }
} }
// ---- // ----
// Warning 6328: (82-96): Assertion violation happens here // Warning 6328: (82-96): Assertion violation happens here.
// Warning 6328: (148-162): Assertion violation happens here // Warning 6328: (148-162): Assertion violation happens here.
// Warning 6328: (180-194): Assertion violation happens here // Warning 6328: (180-194): Assertion violation happens here.
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here.
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here // Warning 4144: (100-103): Underflow (resulting value less than 0) happens here.

8
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol
View File

@ -21,7 +21,7 @@ contract C{
} }
// ---- // ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (234-237): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (234-237): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (234-237): Underflow (resulting value less than 0) happens here // Warning 4144: (234-237): Underflow (resulting value less than 0) happens here.

14
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
View File

@ -21,10 +21,10 @@ contract C{
} }
// ---- // ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (138-152): Assertion violation happens here // Warning 6328: (138-152): Assertion violation happens here.
// Warning 6328: (184-198): Assertion violation happens here // Warning 6328: (184-198): Assertion violation happens here.
// Warning 6328: (82-96): Assertion violation happens here // Warning 6328: (82-96): Assertion violation happens here.
// Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (156-159): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (234-237): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 2661: (234-237): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (234-237): Underflow (resulting value less than 0) happens here // Warning 4144: (234-237): Underflow (resulting value less than 0) happens here.

4
test/libsolidity/smtCheckerTests/functions/library_constant.sol
View File

@ -19,7 +19,7 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (136-155): Assertion violation happens here // Warning 6328: (136-155): Assertion violation happens here.
// Warning 4984: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1) // Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1)

2
test/libsolidity/smtCheckerTests/functions/this_external_call.sol
View File

@ -14,4 +14,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (227-243): Assertion violation happens here // Warning 6328: (227-243): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol
View File

@ -15,4 +15,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (263-279): Assertion violation happens here // Warning 6328: (263-279): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/this_fake.sol
View File

@ -21,4 +21,4 @@ contract C
} }
// ---- // ----
// Warning 2319: (160-166): This declaration shadows a builtin symbol. // Warning 2319: (160-166): This declaration shadows a builtin symbol.
// Warning 6328: (268-282): Assertion violation happens here // Warning 6328: (268-282): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/this_state.sol
View File

@ -14,4 +14,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (186-200): Assertion violation happens here // Warning 6328: (186-200): Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol
View File

@ -25,5 +25,5 @@ contract A is B {
} }
} }
// ---- // ----
// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (328-342): Assertion violation happens here // Warning 6328: (328-342): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol
View File

@ -8,4 +8,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (97-111): Assertion violation happens here // Warning 6328: (97-111): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol
View File

@ -11,4 +11,4 @@ contract D is C {
} }
} }
// ---- // ----
// Warning 6328: (117-131): Assertion violation happens here // Warning 6328: (117-131): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol
View File

@ -19,4 +19,4 @@ contract D is C {
} }
} }
// ---- // ----
// Warning 6328: (211-225): Assertion violation happens here // Warning 6328: (211-225): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol
View File

@ -18,4 +18,4 @@ contract D is C {
} }
} }
// ---- // ----
// Warning 6328: (185-199): Assertion violation happens here // Warning 6328: (185-199): Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
View File

@ -22,10 +22,10 @@ contract A is B {
} }
// ---- // ----
// Warning 4984: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (275-293): Assertion violation happens here // Warning 6328: (275-293): Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
View File

@ -22,9 +22,9 @@ contract A is B {
} }
// ---- // ----
// Warning 4984: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here // Warning 4984: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (273-291): Assertion violation happens here // Warning 6328: (273-291): Assertion violation happens here.

Some files were not shown because too many files have changed in this diff Show More