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 to the tests

Browse Source
This commit is contained in:
Martin Blicha 2023-06-27 11:50:24 +02:00
parent 58d0579ba6
commit c90b48af02
13 changed files with 92 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -28,6 +28,8 @@ contract C {
// ---- // ----
// Warning 6328: (334-364): CHC: Assertion violation happens here. // Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation happens here. // Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here. // Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here. // Warning 4661: (1086-1116): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -28,6 +28,8 @@ contract C {
// ---- // ----
// Warning 6328: (335-365): CHC: Assertion violation happens here. // Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here. // Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here. // Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here. // Warning 4661: (1087-1117): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View File

@ -16,8 +16,7 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// ---- // ----
// Warning 6328: (193-226): CHC: Assertion violation might happen here. // Warning 6328: (193-226): CHC: Assertion violation happens here.
// Warning 6328: (245-279): CHC: Assertion violation happens here. // Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here. // Warning 6328: (298-332): CHC: Assertion violation happens here.
// Warning 1236: (141-156): BMC: Insufficient funds happens here. // Warning 1236: (141-156): BMC: Insufficient funds happens here.
// Warning 4661: (193-226): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View File

@ -21,8 +21,10 @@ contract C {
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (215-233): CHC: Assertion violation might happen here. // Warning 6328: (167-185): CHC: Assertion violation might happen here.
// Warning 6328: (267-285): CHC: Assertion violation might happen here.
// Warning 6328: (304-322): CHC: Assertion violation happens here. // Warning 6328: (304-322): CHC: Assertion violation happens here.
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (215-233): BMC: Assertion violation happens here. // Warning 4661: (167-185): BMC: Assertion violation happens here.
// Warning 4661: (267-285): BMC: Assertion violation happens here.

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

@ -32,5 +32,5 @@ contract C {
// SMTEngine: chc // SMTEngine: chc
// SMTExtCalls: trusted // SMTExtCalls: trusted
// ---- // ----
// Warning 6328: (355-381): CHC: Assertion violation might happen here.
// Warning 6328: (385-399): CHC: Assertion violation might happen here. // Warning 6328: (385-399): CHC: Assertion violation might happen here.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

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

@ -18,4 +18,6 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 6328: (167-181): CHC: Assertion violation might happen here.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 4661: (167-181): BMC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol
View File

@ -14,13 +14,7 @@ contract C is B {
} }
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTSolvers: smtlib2 // SMTSolvers: z3
// ---- // ----
// Warning 6328: (b.sol:62-75): CHC: Assertion violation might happen here. // Warning 6328: (b.sol:62-75): CHC: Assertion violation happens here.
// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. // Warning 6328: (c.sol:68-81): CHC: Assertion violation happens here.
// Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
// Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here.
// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
// Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.

4
test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
View File

@ -23,6 +23,4 @@ contract C {
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6328: (335-354): CHC: Assertion violation might happen here. // Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 4661: (335-354): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
View File

@ -45,4 +45,5 @@ contract C
// Warning 6368: (850-866): CHC: Out of bounds access happens here. // Warning 6368: (850-866): CHC: Out of bounds access happens here.
// Warning 6368: (850-869): CHC: Out of bounds access happens here. // Warning 6368: (850-869): CHC: Out of bounds access happens here.
// Warning 6328: (936-956): CHC: Assertion violation happens here. // Warning 6328: (936-956): CHC: Assertion violation happens here.
// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 6368: (1029-1043): CHC: Out of bounds access might happen here.
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
View File

@ -32,5 +32,6 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here. // Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1391: CHC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

53
test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
View File

@ -53,4 +53,55 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Info 1391: CHC: 51 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 6368: (212-217): CHC: Out of bounds access might happen here.
// Warning 6368: (234-239): CHC: Out of bounds access might happen here.
// Warning 6328: (227-247): CHC: Assertion violation might happen here.
// Warning 6368: (251-256): CHC: Out of bounds access might happen here.
// Warning 6368: (275-280): CHC: Out of bounds access might happen here.
// Warning 6328: (268-290): CHC: Assertion violation might happen here.
// Warning 6368: (294-299): CHC: Out of bounds access might happen here.
// Warning 6368: (312-317): CHC: Out of bounds access might happen here.
// Warning 6368: (330-335): CHC: Out of bounds access might happen here.
// Warning 6368: (348-353): CHC: Out of bounds access might happen here.
// Warning 6368: (348-358): CHC: Out of bounds access might happen here.
// Warning 6368: (373-378): CHC: Out of bounds access might happen here.
// Warning 6368: (373-383): CHC: Out of bounds access might happen here.
// Warning 6328: (366-389): CHC: Assertion violation might happen here.
// Warning 6368: (393-398): CHC: Out of bounds access might happen here.
// Warning 6368: (412-417): CHC: Out of bounds access might happen here.
// Warning 6368: (431-436): CHC: Out of bounds access might happen here.
// Warning 6368: (450-455): CHC: Out of bounds access might happen here.
// Warning 6368: (469-474): CHC: Out of bounds access might happen here.
// Warning 6368: (488-493): CHC: Out of bounds access might happen here.
// Warning 6368: (488-499): CHC: Out of bounds access might happen here.
// Warning 6368: (516-521): CHC: Out of bounds access might happen here.
// Warning 6368: (516-527): CHC: Out of bounds access might happen here.
// Warning 6328: (509-535): CHC: Assertion violation might happen here.
// Warning 6368: (539-544): CHC: Out of bounds access might happen here.
// Warning 6368: (558-563): CHC: Out of bounds access might happen here.
// Warning 6368: (577-582): CHC: Out of bounds access might happen here.
// Warning 6368: (596-601): CHC: Out of bounds access might happen here.
// Warning 6368: (615-620): CHC: Out of bounds access might happen here.
// Warning 6368: (634-639): CHC: Out of bounds access might happen here.
// Warning 6368: (634-645): CHC: Out of bounds access might happen here.
// Warning 6368: (658-663): CHC: Out of bounds access might happen here.
// Warning 6368: (658-669): CHC: Out of bounds access might happen here.
// Warning 6368: (682-687): CHC: Out of bounds access might happen here.
// Warning 6368: (682-693): CHC: Out of bounds access might happen here.
// Warning 6368: (706-711): CHC: Out of bounds access might happen here.
// Warning 6368: (706-717): CHC: Out of bounds access might happen here.
// Warning 6368: (730-735): CHC: Out of bounds access might happen here.
// Warning 6368: (730-741): CHC: Out of bounds access might happen here.
// Warning 6368: (754-759): CHC: Out of bounds access might happen here.
// Warning 6368: (754-765): CHC: Out of bounds access might happen here.
// Warning 6368: (778-783): CHC: Out of bounds access might happen here.
// Warning 6368: (778-789): CHC: Out of bounds access might happen here.
// Warning 6368: (778-794): CHC: Out of bounds access might happen here.
// Warning 6368: (809-814): CHC: Out of bounds access might happen here.
// Warning 6368: (809-820): CHC: Out of bounds access might happen here.
// Warning 6368: (809-825): CHC: Out of bounds access might happen here.
// Warning 6328: (802-831): CHC: Assertion violation might happen here.
// Warning 2529: (835-843): CHC: Empty array "pop" might happen here.
// Warning 2529: (847-855): CHC: Empty array "pop" might happen here.
// Warning 2529: (859-867): CHC: Empty array "pop" might happen here.
// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol
View File

@ -17,5 +17,4 @@ contract C
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6368: (216-225): CHC: Out of bounds access might happen here. // Info 1391: CHC: 10 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

16
test/libsolidity/smtCheckerTests/types/type_minmax.sol
View File

@ -82,4 +82,18 @@ contract C {
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (178-207): CHC: Assertion violation happens here. // Warning 6328: (178-207): CHC: Assertion violation happens here.
// Info 1391: CHC: 24 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 6328: (872-900): CHC: Assertion violation might happen here.
// Warning 6328: (942-970): CHC: Assertion violation might happen here.
// Warning 6328: (1015-1045): CHC: Assertion violation might happen here.
// Warning 6328: (1125-1147): CHC: Assertion violation might happen here.
// Warning 6328: (1192-1215): CHC: Assertion violation might happen here.
// Warning 6328: (1260-1283): CHC: Assertion violation might happen here.
// Warning 6328: (1328-1351): CHC: Assertion violation might happen here.
// Warning 6328: (1399-1423): CHC: Assertion violation might happen here.
// Warning 6328: (1503-1530): CHC: Assertion violation might happen here.
// Warning 6328: (1575-1604): CHC: Assertion violation might happen here.
// Warning 6328: (1649-1678): CHC: Assertion violation might happen here.
// Warning 6328: (1723-1752): CHC: Assertion violation might happen here.
// Warning 6328: (1800-1831): CHC: Assertion violation might happen here.
// Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 6002: BMC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.