cerc-io/solidity
10
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

Add non-revert condition.

Browse Source
This commit is contained in:
chriseth 2022-03-03 14:05:15 +01:00
parent fdee68f1b4
commit 63c74f5da2
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
test/formal/redundant_store_unrelated.py
View File

@ -3,8 +3,8 @@ import sys
"""
Tests that the conditions inside RedundantStoreEliminator::knownUnrelated
properly account for overflow.
only return "unrelated" incorrectly if one of the operation reverts
due to large memory access.
"""
n_bits = 256
@ -34,7 +34,13 @@ restrict(diff)
# These are the conditions in the code.
solver.add(diff >= length1)
solver.add(diff <= 2**n_bits - length2)
solver.add(diff <= 2**(n_bits-1))
# If start1 >= 2**(n_bits-1), the operation will revert,
# so we assume the converse.
solver.add(start1 < 2**(n_bits-1))
# Now there should be no overlap:
# x is a potential point where the memory operations
# overlap.