Skip to content

Commit 0cc9162

Browse files
author
Leo Alt
committed
Update SMTChecker tests
1 parent 4d414a6 commit 0cc9162

File tree

62 files changed

+0
-350
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+0
-350
lines changed

‎test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,3 @@ contract C {
88
// ----
99
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
1010
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)
11-
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
12-
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)

‎test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -59,20 +59,6 @@ contract C {
5959
// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
6060
// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
6161
// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
62-
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
63-
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
64-
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
65-
// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
66-
// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
67-
// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
68-
// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
69-
// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
70-
// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
71-
// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
72-
// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
73-
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
74-
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
75-
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
7662
// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
7763
// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
7864
// Warning 4661: (1103-1131): BMC: Assertion violation happens here.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,3 @@ contract C {
77
// SMTEngine: all
88
// ----
99
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.
10-
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,3 @@ contract C {
2424
// ----
2525
// Warning 6328: (315-331): CHC: Assertion violation happens here.
2626
// Warning 1236: (87-100): BMC: Insufficient funds happens here.
27-
// Warning 1236: (87-100): BMC: Insufficient funds happens here.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,4 +21,3 @@ contract C {
2121
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
2222
// Warning 6328: (263-279): CHC: Assertion violation happens here.
2323
// Warning 6328: (359-373): CHC: Assertion violation happens here.
24-
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,3 @@ contract C {
2424
// Warning 6328: (282-298): CHC: Assertion violation happens here.
2525
// Warning 6328: (317-331): CHC: Assertion violation happens here.
2626
// Warning 1236: (54-67): BMC: Insufficient funds happens here.
27-
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,4 +26,3 @@ contract C {
2626
// Warning 6328: (309-325): CHC: Assertion violation happens here.
2727
// Warning 6328: (405-419): CHC: Assertion violation happens here.
2828
// Warning 6328: (464-486): CHC: Assertion violation happens here.
29-
// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,4 +27,3 @@ contract C {
2727
// Warning 6328: (316-332): CHC: Assertion violation happens here.
2828
// Warning 6328: (412-426): CHC: Assertion violation happens here.
2929
// Warning 6328: (471-494): CHC: Assertion violation happens here.
30-
// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/bmc_coverage/unchecked_function_call_with_unchecked_block.sol

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,4 +13,3 @@ contract C {
1313
// SMTEngine: bmc
1414
// ----
1515
// Warning 4661: (85-98): BMC: Assertion violation happens here.
16-
// Warning 4661: (85-98): BMC: Assertion violation happens here.

‎test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,4 @@ contract InternalCall {
8585
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
8686
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
8787
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
88-
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
89-
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
9088
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

0 commit comments

Comments
 (0)