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 smtchecker tests

Browse Source
This commit is contained in:
Leo Alt 2023-03-28 14:36:56 +02:00
parent 3e1e43f569
commit ce9a7ee954
8 changed files with 9 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.circleci/config.yml
View File

@ -26,7 +26,7 @@ parameters:
emscripten-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-15
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f86cb1fb4631b1fbb927149f60caea7b095be5b85d379456eee09cb105e7f225"
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e2729bd6c0734bb49d04e2688fec3dcf880394f351f69358dd2bd92c0f6fd309"
evm-version:
type: string
default: london

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

@ -28,8 +28,8 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 6368: (238-242): CHC: Out of bounds access happens here.
// Warning 6368: (238-245): CHC: Out of bounds access might happen here.
// Warning 6368: (238-248): CHC: Out of bounds access might happen here.
// Warning 6368: (238-245): CHC: Out of bounds access happens here.
// Warning 6368: (238-248): CHC: Out of bounds access happens here.
// Warning 6368: (311-315): CHC: Out of bounds access happens here.
// Warning 6368: (343-347): CHC: Out of bounds access happens here.
// Warning 6328: (336-360): CHC: Assertion violation happens here.

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

@ -24,9 +24,8 @@ contract C {
// Warning 6328: (167-185): CHC: Assertion violation might happen here.
// Warning 6328: (215-233): CHC: Assertion violation might happen here.
// Warning 6328: (267-285): CHC: Assertion violation might happen here.
// Warning 6328: (304-322): CHC: Assertion violation might happen here.
// Warning 6328: (304-322): CHC: Assertion violation happens here.
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (167-185): BMC: Assertion violation happens here.
// Warning 4661: (215-233): BMC: Assertion violation happens here.
// Warning 4661: (267-285): BMC: Assertion violation happens here.
// Warning 4661: (304-322): BMC: Assertion violation happens here.

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

@ -18,6 +18,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// 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.
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

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

@ -21,6 +21,7 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 6328: (335-354): CHC: Assertion violation 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.

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

@ -34,6 +34,7 @@ contract C
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 6368: (439-453): CHC: Out of bounds access happens here.
// Warning 6368: (465-480): CHC: Out of bounds access might happen here.

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

@ -34,5 +34,4 @@ contract C
// Warning 6368: (612-627): CHC: Out of bounds access might happen here.
// Warning 6328: (860-880): CHC: Assertion violation happens here.
// Warning 6368: (936-952): CHC: Out of bounds access might happen here.
// Warning 6368: (936-955): CHC: Out of bounds access might happen here.
// Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 7 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,6 +32,5 @@ contract C {
// SMTEngine: all
// 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.
// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.