diff --git a/.circleci/config.yml b/.circleci/config.yml index 18f0ec2d0..e189ea07b 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol index 3a57c40cb..ebabc9706 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index ddd4b41e6..dcc81be64 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index fd45ef2d7..593aba289 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol index d3b6f5895..d18f605f7 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index a2fc893b5..fce586987 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index 0b85a71b4..1f167b858 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index d89f020ae..bb4ef0342 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -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.