Skip to content

Commit 5bfa17e

Browse files
docs: fix value boundary
Using `val = val % token.balanceOf(address(this))` constrains the value to be from zero up to the `token.balanceOf(address(this))` (not included). It misses the maximal value of `token.balanceOf(address(this))`.
1 parent 93e7f0e commit 5bfa17e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

program-analysis/echidna/property-creation.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ We want Echidna to spend most of the execution exploring the contract to test. S
162162
```solidity
163163
function depositShares_never_reverts(uint256 val) public {
164164
if(token.balanceOf(address(this)) > 0) {
165-
val = val % token.balanceOf(address(this));
165+
val = val % (token.balanceOf(address(this)) + 1);
166166
try c.depositShares(val) { /* not reverted */ } catch { assert(false); }
167167
assert(c.getShares(address(this)) > 0);
168168
} else {

0 commit comments

Comments
 (0)