Skip to content

Commit 85378b1

Browse files
author
Leo Alt
committed
Update existing tests
1 parent 563469a commit 85378b1

File tree

68 files changed

+177
-95
lines changed

Some content is hidden

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

68 files changed

+177
-95
lines changed

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

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,16 +45,19 @@ contract C {
4545
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
4646
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
4747
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
48+
// Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver.
49+
// Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver.
50+
// Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver.
4851
// Warning 6328: (182-210): CHC: Assertion violation happens here.
4952
// Warning 6328: (335-363): CHC: Assertion violation happens here.
5053
// Warning 6328: (414-442): CHC: Assertion violation happens here.
5154
// Warning 6328: (560-588): CHC: Assertion violation happens here.
5255
// Warning 6328: (607-635): CHC: Assertion violation happens here.
5356
// Warning 6328: (654-682): CHC: Assertion violation happens here.
5457
// Warning 6328: (879-916): CHC: Assertion violation happens here.
55-
// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
56-
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
57-
// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
58+
// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
59+
// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
60+
// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
5861
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
5962
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
6063
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
@@ -69,3 +72,6 @@ contract C {
6972
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
7073
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
7174
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
75+
// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
76+
// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
77+
// Warning 4661: (1103-1131): BMC: Assertion violation happens here.

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,14 @@ contract C {
2121
// SMTEngine: all
2222
// SMTIgnoreCex: yes
2323
// ----
24+
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
25+
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
2426
// Warning 6328: (209-223): CHC: Assertion violation happens here.
2527
// Warning 6328: (260-274): CHC: Assertion violation happens here.
2628
// Warning 6328: (359-373): CHC: Assertion violation happens here.
2729
// Warning 6328: (392-406): CHC: Assertion violation happens here.
2830
// Warning 6328: (425-434): CHC: Assertion violation happens here.
29-
// Warning 6328: (505-519): CHC: Assertion violation happens here.
30-
// Warning 6328: (538-552): CHC: Assertion violation happens here.
31+
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
32+
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
33+
// Warning 4661: (505-519): BMC: Assertion violation happens here.
34+
// Warning 4661: (538-552): BMC: Assertion violation happens here.

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

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,15 @@ contract C {
2323
// ====
2424
// SMTEngine: all
2525
// ----
26-
// Warning 6328: (322-352): CHC: Assertion violation happens here.
27-
// Warning 6328: (419-449): CHC: Assertion violation happens here.
28-
// Warning 6328: (528-558): CHC: Assertion violation happens here.
29-
// Warning 6328: (577-607): CHC: Assertion violation happens here.
26+
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
27+
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
28+
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
29+
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
30+
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
31+
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
32+
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
33+
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
34+
// Warning 4661: (322-352): BMC: Assertion violation happens here.
35+
// Warning 4661: (419-449): BMC: Assertion violation happens here.
36+
// Warning 4661: (528-558): BMC: Assertion violation happens here.
37+
// Warning 4661: (577-607): BMC: Assertion violation happens here.

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,15 +22,17 @@ contract C {
2222
// ====
2323
// SMTEngine: all
2424
// ----
25+
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
2526
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
2627
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
2728
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
2829
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
29-
// Warning 6328: (226-256): CHC: Assertion violation happens here.
30+
// Warning 6328: (226-256): CHC: Assertion violation might happen here.
3031
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
3132
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
3233
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
3334
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
35+
// Warning 4661: (226-256): BMC: Assertion violation happens here.
3436
// Warning 4661: (310-340): BMC: Assertion violation happens here.
3537
// Warning 4661: (483-513): BMC: Assertion violation happens here.
3638
// Warning 4661: (568-598): BMC: Assertion violation happens here.

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,13 @@ contract C {
2323
// SMTEngine: all
2424
// SMTShowUnproved: no
2525
// ----
26+
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
2627
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
2728
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
2829
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
2930
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
30-
// Warning 6328: (226-256): CHC: Assertion violation happens here.
31-
// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
31+
// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
32+
// Warning 4661: (226-256): BMC: Assertion violation happens here.
3233
// Warning 4661: (310-340): BMC: Assertion violation happens here.
3334
// Warning 4661: (483-513): BMC: Assertion violation happens here.
3435
// Warning 4661: (568-598): BMC: Assertion violation happens here.

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

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,12 @@ contract C {
2020
// ====
2121
// SMTEngine: all
2222
// ----
23-
// Warning 6328: (298-328): CHC: Assertion violation happens here.
24-
// Warning 6328: (389-419): CHC: Assertion violation happens here.
25-
// Warning 6328: (492-522): CHC: Assertion violation happens here.
23+
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
24+
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
25+
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
26+
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
27+
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
28+
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
29+
// Warning 4661: (298-328): BMC: Assertion violation happens here.
30+
// Warning 4661: (389-419): BMC: Assertion violation happens here.
31+
// Warning 4661: (492-522): BMC: Assertion violation happens here.

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,15 @@ contract C {
1919
// ====
2020
// SMTEngine: all
2121
// ----
22+
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
2223
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
2324
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
2425
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
25-
// Warning 6328: (208-238): CHC: Assertion violation happens here.
26+
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
2627
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
2728
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
2829
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
30+
// Warning 4661: (208-238): BMC: Assertion violation happens here.
2931
// Warning 4661: (286-316): BMC: Assertion violation happens here.
3032
// Warning 4661: (453-483): BMC: Assertion violation happens here.
3133
// Warning 4661: (532-562): BMC: Assertion violation happens here.

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,14 +25,16 @@ contract C {
2525
// ====
2626
// SMTEngine: all
2727
// ----
28+
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
2829
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
2930
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
3031
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
3132
// Warning 6328: (325-355): CHC: Assertion violation happens here.
32-
// Warning 6328: (578-608): CHC: Assertion violation happens here.
33+
// Warning 6328: (578-608): CHC: Assertion violation might happen here.
3334
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
3435
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
3536
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
37+
// Warning 4661: (578-608): BMC: Assertion violation happens here.
3638
// Warning 4661: (691-721): BMC: Assertion violation happens here.
3739
// Warning 4661: (959-989): BMC: Assertion violation happens here.
3840
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,14 +25,16 @@ contract C {
2525
// ====
2626
// SMTEngine: all
2727
// ----
28+
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
2829
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
2930
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
3031
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
3132
// Warning 6328: (326-356): CHC: Assertion violation happens here.
32-
// Warning 6328: (579-609): CHC: Assertion violation happens here.
33+
// Warning 6328: (579-609): CHC: Assertion violation might happen here.
3334
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
3435
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
3536
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
37+
// Warning 4661: (579-609): BMC: Assertion violation happens here.
3638
// Warning 4661: (692-722): BMC: Assertion violation happens here.
3739
// Warning 4661: (960-990): BMC: Assertion violation happens here.
3840
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

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

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ contract C {
2525
// SMTEngine: all
2626
// ----
2727
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
28-
// Warning 6328: (571-601): CHC: Assertion violation happens here.
28+
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
29+
// Warning 6328: (571-601): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
2930
// Warning 6328: (691-721): CHC: Assertion violation happens here.
30-
// Warning 6328: (740-770): CHC: Assertion violation happens here.
31-
// Warning 6328: (855-885): CHC: Assertion violation happens here.
31+
// Warning 6328: (740-770): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
32+
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
33+
// Warning 4661: (855-885): BMC: Assertion violation happens here.

0 commit comments

Comments
 (0)