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

Update tests

Browse Source
This commit is contained in:
Leonardo Alt 2020-07-13 20:48:00 +02:00
parent 51721c3080
commit 003c9b9a5b
215 changed files with 305 additions and 325 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -11,10 +11,10 @@ contract C {
}
}
// ----
// Warning 6328: (119-157): Assertion violation happens here
// Warning 8115: (76-80): Assertion checker does not yet support the type of this variable.
// Warning 8115: (83-87): Assertion checker does not yet support the type of this variable.
// Warning 7650: (126-132): Assertion checker does not yet support this expression.
// Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (143-149): Assertion checker does not yet support this expression.
// Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4661: (119-157): Assertion violation happens here

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

@ -11,6 +11,7 @@ contract C {
}
}
// ----
// Warning 6328: (121-165): Assertion violation happens here
// Warning 8115: (78-82): Assertion checker does not yet support the type of this variable.
// Warning 8115: (85-89): Assertion checker does not yet support the type of this variable.
// Warning 7650: (128-134): Assertion checker does not yet support this expression.
@ -19,4 +20,3 @@ contract C {
// Warning 7650: (148-154): Assertion checker does not yet support this expression.
// Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref
// Warning 9118: (148-157): Assertion checker does not yet implement this expression.
// Warning 4661: (121-165): Assertion violation happens here

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

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 4661: (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 4661: (198-224): Assertion violation happens here
// Warning 4661: (228-254): Assertion violation happens here
// Warning 4661: (258-281): Assertion violation happens here
// Warning 6328: (198-224): Assertion violation happens here
// Warning 6328: (228-254): 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 4661: (222-248): Assertion violation happens here
// Warning 4661: (252-278): Assertion violation happens here
// Warning 4661: (282-305): Assertion violation happens here
// Warning 4661: (309-335): Assertion violation happens here
// Warning 6328: (222-248): Assertion violation happens here
// Warning 6328: (252-278): Assertion violation happens here
// Warning 6328: (282-305): 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_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

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

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

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

@ -12,5 +12,5 @@ contract C {
}
}
// ----
// Warning 6328: (205-239): Assertion violation happens here
// Warning 4144: (217-232): Underflow (resulting value less than 0) happens here
// Warning 4661: (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 4661: (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 4661: (193-217): Assertion violation happens here
// Warning 4661: (309-333): Assertion violation happens here
// Warning 4661: (419-436): Assertion violation happens here
// Warning 6328: (193-217): Assertion violation happens here
// Warning 6328: (309-333): 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 4661: (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 4661: (94-124): Assertion violation happens here
// Warning 6328: (94-124): Assertion violation happens here

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

@ -15,5 +15,5 @@ contract c {
}
}
// ----
// Warning 6328: (227-236): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (227-236): Assertion violation happens here

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

@ -17,6 +17,6 @@ contract c {
}
}
// ----
// Warning 6328: (202-218): Assertion violation happens here
// Warning 6328: (242-252): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (202-218): Assertion violation happens here
// Warning 4661: (242-252): Assertion violation happens here

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

@ -15,5 +15,5 @@ contract c {
}
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (225-235): Assertion violation happens here

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

@ -15,5 +15,5 @@ contract c {
}
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (225-235): Assertion violation happens here

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

@ -24,5 +24,5 @@ contract c {
}
}
// ----
// Warning 6328: (360-370): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (360-370): Assertion violation happens here

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

@ -15,5 +15,5 @@ contract c {
}
}
// ----
// Warning 6328: (225-235): Assertion violation happens here
// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (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 4661: (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 4661: (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 4661: (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 4661: (200-214): Assertion violation happens here
// Warning 6328: (200-214): Assertion violation happens here

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

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

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

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

2
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 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (189-203): Assertion violation happens here

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

@ -25,4 +25,4 @@ contract C {
}
}
// ----
// Warning 4661: (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 4661: (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 4661: (307-321): Assertion violation happens here
// Warning 6328: (307-321): Assertion violation happens here

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

@ -9,5 +9,4 @@ contract C {
}
}
// ----
// Warning 4661: (116-132): Assertion violation happens here
// Warning 4661: (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 4661: (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 4661: (209-223): Assertion violation happens here
// Warning 4661: (321-335): Assertion violation happens here
// Warning 6328: (209-223): 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 4661: (261-277): Assertion violation happens here
// Warning 6328: (261-277): Assertion violation happens here

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

@ -16,4 +16,4 @@ contract D
}
}
// ----
// Warning 4661: (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 4661: (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 4661: (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 4661: (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 8364: (228-229): Assertion checker does not yet implement type type(library L)
// Warning 4661: (245-261): Assertion violation happens here

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

@ -13,4 +13,4 @@ contract C
}
// ----
// Warning 4661: (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 4661: (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 4661: (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 4661: (274-288): Assertion violation happens here
// Warning 6328: (274-288): Assertion violation happens here

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

@ -17,9 +17,10 @@ contract C is A {
}
}
// ----
// Warning 4661: (82-96): Assertion violation happens here
// Warning 6328: (82-96): Assertion violation happens here
// Warning 6328: (155-169): Assertion violation happens here
// Warning 6328: (187-201): Assertion violation happens here
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here
// Warning 4661: (82-96): Assertion violation happens here
// Warning 4144: (100-103): Underflow (resulting value less than 0) happens here
// Warning 4661: (148-162): Assertion violation happens here
// Warning 4661: (82-96): Assertion violation happens here

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

@ -19,7 +19,7 @@ contract C {
}
}
// ----
// Warning 4661: (136-155): Assertion violation happens here
// Warning 6328: (136-155): Assertion violation happens here
// Warning 2661: (229-234): 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 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here

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

@ -9,6 +9,9 @@ contract C
function g(uint y) public {
require(y < 1000);
this.f(y);
// Fails as false positive because CHC does not support `this`.
assert(x < 1000);
}
}
// ----
// Warning 6328: (227-243): Assertion violation happens here

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

@ -10,6 +10,9 @@ contract C
function g(uint y) public {
require(y < 1000);
uint z = this.f(y);
// Fails as false positive because CHC does not support `this`.
assert(z < 1000);
}
}
// ----
// 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 4661: (268-282): Assertion violation happens here
// Warning 6328: (268-282): Assertion violation happens here

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

@ -6,10 +6,12 @@ contract C
function g() public {
x = 0;
this.h();
// Function call is inlined.
// Fails as false positive because CHC does not support `this`.
assert(x == 2);
}
function h() public {
x = 2;
}
}
// ----
// Warning 6328: (186-200): Assertion violation happens here

7
test/libsolidity/smtCheckerTests/inheritance/fallback.sol
View File

@ -21,7 +21,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (122-136): Assertion violation happens here
// Warning 4661: (171-185): Assertion violation happens here
// Warning 4661: (288-302): Assertion violation happens here
// Warning 4661: (171-185): Assertion violation happens here
// Warning 6328: (122-136): Assertion violation happens here
// Warning 6328: (171-185): Assertion violation happens here
// Warning 6328: (288-302): Assertion violation happens here

8
test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
View File

@ -21,8 +21,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (114-128): Assertion violation happens here
// Warning 4661: (163-177): Assertion violation happens here
// Warning 4661: (289-303): Assertion violation happens here
// Warning 4661: (114-128): Assertion violation happens here
// Warning 4661: (163-177): Assertion violation happens here
// Warning 6328: (114-128): Assertion violation happens here
// Warning 6328: (163-177): Assertion violation happens here
// Warning 6328: (289-303): Assertion violation happens here

7
test/libsolidity/smtCheckerTests/inheritance/functions_1.sol
View File

@ -19,7 +19,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (121-135): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 4661: (276-290): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 6328: (121-135): Assertion violation happens here
// Warning 6328: (170-184): Assertion violation happens here
// Warning 6328: (276-290): Assertion violation happens here

7
test/libsolidity/smtCheckerTests/inheritance/functions_2.sol
View File

@ -21,7 +21,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (121-135): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 4661: (286-300): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 6328: (121-135): Assertion violation happens here
// Warning 6328: (170-184): Assertion violation happens here
// Warning 6328: (286-300): Assertion violation happens here

15
test/libsolidity/smtCheckerTests/inheritance/functions_3.sol
View File

@ -36,12 +36,9 @@ contract C is B {
}
}
// ----
// Warning 4661: (121-135): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 4661: (296-310): Assertion violation happens here
// Warning 4661: (345-359): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 4661: (468-482): Assertion violation happens here
// Warning 4661: (517-531): Assertion violation happens here
// Warning 4661: (345-359): Assertion violation happens here
// Warning 4661: (170-184): Assertion violation happens here
// Warning 6328: (121-135): Assertion violation happens here
// Warning 6328: (170-184): Assertion violation happens here
// Warning 6328: (296-310): Assertion violation happens here
// Warning 6328: (345-359): Assertion violation happens here
// Warning 6328: (468-482): Assertion violation happens here
// Warning 6328: (517-531): Assertion violation happens here

7
test/libsolidity/smtCheckerTests/inheritance/receive.sol
View File

@ -21,7 +21,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (128-142): Assertion violation happens here
// Warning 4661: (177-191): Assertion violation happens here
// Warning 4661: (300-314): Assertion violation happens here
// Warning 4661: (177-191): Assertion violation happens here
// Warning 6328: (128-142): Assertion violation happens here
// Warning 6328: (177-191): Assertion violation happens here
// Warning 6328: (300-314): Assertion violation happens here

8
test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol
View File

@ -21,8 +21,6 @@ contract B is A {
}
}
// ----
// Warning 4661: (120-134): Assertion violation happens here
// Warning 4661: (169-183): Assertion violation happens here
// Warning 4661: (288-302): Assertion violation happens here
// Warning 4661: (120-134): Assertion violation happens here
// Warning 4661: (169-183): Assertion violation happens here
// Warning 6328: (120-134): Assertion violation happens here
// Warning 6328: (169-183): Assertion violation happens here
// Warning 6328: (288-302): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
View File

@ -31,4 +31,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (311-324): Assertion violation happens here
// Warning 6328: (311-324): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
View File

@ -14,5 +14,5 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 6328: (179-193): Assertion violation happens here
// Warning 2661: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (179-193): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol
View File

@ -19,4 +19,4 @@ contract C {
// ----
// Warning 5740: (128-133): Unreachable code.
// Warning 5740: (147-151): Unreachable code.
// Warning 4661: (180-194): Assertion violation happens here
// Warning 6328: (180-194): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol
View File

@ -15,4 +15,4 @@ contract C {
// ----
// Warning 5740: (104-109): Unreachable code.
// Warning 5740: (122-128): Unreachable code.
// Warning 4661: (133-147): Assertion violation happens here
// Warning 6328: (133-147): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol
View File

@ -17,4 +17,4 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (201-216): Assertion violation happens here
// Warning 6328: (201-216): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol
View File

@ -14,4 +14,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5667: (66-72): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 4661: (142-156): Assertion violation happens here
// Warning 6328: (142-156): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
View File

@ -14,5 +14,5 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 6328: (189-203): Assertion violation happens here
// Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (189-203): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_loop_4.sol
View File

@ -9,4 +9,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (136-150): Assertion violation happens here
// Warning 6328: (136-150): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_loop_5.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (167-181): Assertion violation happens here
// Warning 6328: (167-181): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -15,6 +15,6 @@ contract LoopFor2 {
}
}
// ----
// Warning 4661: (281-301): Assertion violation happens here
// Warning 4661: (305-324): Assertion violation happens here
// Warning 4661: (328-347): Assertion violation happens here
// Warning 6328: (281-301): Assertion violation happens here
// Warning 6328: (305-324): Assertion violation happens here
// Warning 6328: (328-347): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol
View File

@ -19,5 +19,5 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (274-294): Assertion violation happens here
// Warning 4661: (321-340): Assertion violation happens here
// Warning 6328: (274-294): Assertion violation happens here
// Warning 6328: (321-340): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
View File

@ -19,4 +19,4 @@ contract LoopFor2 {
}
}
// ----
// Warning 4661: (363-382): Assertion violation happens here
// Warning 6328: (363-382): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
View File

@ -19,5 +19,5 @@ contract LoopFor2 {
}
}
// ----
// Warning 4661: (341-360): Assertion violation happens here
// Warning 4661: (364-383): Assertion violation happens here
// Warning 6328: (341-360): Assertion violation happens here
// Warning 6328: (364-383): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol
View File

@ -18,4 +18,4 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (218-233): Assertion violation happens here
// Warning 6328: (218-233): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol
View File

@ -21,4 +21,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5740: (169-176): Unreachable code.
// Warning 4661: (227-242): Assertion violation happens here
// Warning 6328: (227-242): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_1_fail.sol
View File

@ -13,4 +13,4 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (139-153): Assertion violation happens here
// Warning 6328: (139-153): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
View File

@ -15,4 +15,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5740: (120-123): Unreachable code.
// Warning 4661: (131-145): Assertion violation happens here
// Warning 6328: (131-145): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -19,6 +19,6 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (281-301): Assertion violation happens here
// Warning 4661: (305-324): Assertion violation happens here
// Warning 4661: (328-347): Assertion violation happens here
// Warning 6328: (281-301): Assertion violation happens here
// Warning 6328: (305-324): Assertion violation happens here
// Warning 6328: (328-347): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
View File

@ -23,5 +23,5 @@ contract LoopFor2 {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (362-382): Assertion violation happens here
// Warning 4661: (409-428): Assertion violation happens here
// Warning 6328: (362-382): Assertion violation happens here
// Warning 6328: (409-428): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -21,5 +21,5 @@ contract LoopFor2 {
}
}
// ----
// Warning 4661: (320-339): Assertion violation happens here
// Warning 4661: (343-362): Assertion violation happens here
// Warning 6328: (320-339): Assertion violation happens here
// Warning 6328: (343-362): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
View File

@ -12,4 +12,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (194-208): Assertion violation happens here
// Warning 6328: (194-208): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol
View File

@ -10,4 +10,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (187-201): Assertion violation happens here
// Warning 6328: (187-201): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol
View File

@ -12,4 +12,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning 4661: (224-238): Assertion violation happens here
// Warning 6328: (224-238): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
View File

@ -29,5 +29,5 @@ contract C
}
}
// ----
// Warning 4661: (329-344): Assertion violation happens here
// Warning 4661: (380-395): Assertion violation happens here
// Warning 6328: (329-344): Assertion violation happens here
// Warning 6328: (380-395): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
View File

@ -27,5 +27,5 @@ contract C
}
}
// ----
// Warning 4661: (323-338): Assertion violation happens here
// Warning 4661: (362-377): Assertion violation happens here
// Warning 6328: (323-338): Assertion violation happens here
// Warning 6328: (362-377): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
View File

@ -21,5 +21,5 @@ contract C
}
}
// ----
// Warning 6328: (136-149): Assertion violation happens here
// Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (136-149): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_control_flow.sol
View File

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

2
test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol
View File

@ -20,4 +20,4 @@ contract C {
}
}
// ----
// Warning 4661: (287-300): Assertion violation happens here
// Warning 6328: (287-300): Assertion violation happens here

5
test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol
View File

@ -25,6 +25,8 @@ contract C {
x = y;
if (y > 1) {
f();
// This now fails as a false positive because
// CHC does not propagate msg.sender throughout predicates.
assert(x == y + 1);
}
// Fails for {y = 0, x = 0}.
@ -32,4 +34,5 @@ contract C {
}
}
// ----
// Warning 4661: (461-475): Assertion violation happens here
// Warning 6328: (516-534): Assertion violation happens here
// Warning 6328: (573-587): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol
View File

@ -26,4 +26,4 @@ contract C
}
}
// ----
// Warning 4661: (170-183): Assertion violation happens here
// Warning 6328: (170-183): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol
View File

@ -22,4 +22,4 @@ contract C
}
}
// ----
// Warning 4661: (311-324): Assertion violation happens here
// Warning 6328: (311-324): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol
View File

@ -13,4 +13,4 @@ contract C
}
}
// ----
// Warning 4661: (164-177): Assertion violation happens here
// Warning 6328: (164-177): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol
View File

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 4661: (128-142): Assertion violation happens here
// Warning 6328: (128-142): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol
View File

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 4661: (121-135): Assertion violation happens here
// Warning 6328: (121-135): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol
View File

@ -23,4 +23,4 @@ contract C
}
}
// ----
// Warning 4661: (156-170): Assertion violation happens here
// Warning 6328: (156-170): Assertion violation happens here

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

@ -15,4 +15,4 @@ contract C {
}
}
// ----
// Warning 4661: (104-122): Assertion violation happens here
// Warning 6328: (104-122): Assertion violation happens here

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

@ -9,4 +9,4 @@ contract C {
}
}
// ----
// Warning 4661: (76-94): Assertion violation happens here
// Warning 6328: (76-94): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol
View File

@ -13,6 +13,6 @@ contract C {
}
}
// ----
// Warning 4661: (107-125): Assertion violation happens here
// Warning 4661: (180-203): Assertion violation happens here
// Warning 4661: (207-230): Assertion violation happens here
// Warning 6328: (107-125): Assertion violation happens here
// Warning 6328: (180-203): Assertion violation happens here
// Warning 6328: (207-230): Assertion violation happens here

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

@ -11,4 +11,4 @@ contract C
}
}
// ----
// Warning 4661: (151-166): Assertion violation happens here
// Warning 6328: (151-166): Assertion violation happens here

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

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 4661: (192-214): Assertion violation happens here
// Warning 6328: (192-214): Assertion violation happens here

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

@ -12,4 +12,4 @@ contract C
}
}
// ----
// Warning 4661: (198-218): Assertion violation happens here
// Warning 6328: (198-218): Assertion violation happens here

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

@ -9,5 +9,5 @@ contract C {
}
}
// ----
// Warning 6328: (116-130): Assertion violation happens here
// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.
// Warning 4661: (116-130): Assertion violation happens here

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

@ -9,5 +9,5 @@ contract C {
}
}
// ----
// Warning 6328: (116-130): Assertion violation happens here
// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.
// Warning 4661: (116-130): Assertion violation happens here

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

@ -11,4 +11,4 @@ contract C
}
}
// ----
// Warning 4661: (150-164): Assertion violation happens here
// Warning 6328: (150-164): Assertion violation happens here

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