NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added assert message

Browse Source
This commit is contained in:
Thomas Adams
2022-05-26 14:35:27 -07:00
parent 1dd3b7a307
commit 4dc0ff9fe3
1 changed files with 5 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
certora/specs/ERC1155Burnable.spec
View File

@ -3,9 +3,9 @@ methods {
isApprovedForAll(address,address) returns bool envfree isApprovedForAll(address,address) returns bool envfree
} }
/// If a method call reduces account balances, the caller should be either the /// If a method call reduces account balances, the caller must be either the
/// owner of the account or approved by the owner to act on its behalf. /// owner of the account or approved by the owner to act on the owner's behalf.
rule onlyApprovedCanReduceBalance { rule onlyHolderOrApprovedCanReduceBalance {
address holder; uint256 token; uint256 amount; address holder; uint256 token; uint256 amount;
uint256 balanceBefore = balanceOf(holder, token); uint256 balanceBefore = balanceOf(holder, token);
@ -14,7 +14,8 @@ rule onlyApprovedCanReduceBalance {
uint256 balanceAfter = balanceOf(holder, token); uint256 balanceAfter = balanceOf(holder, token);
assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender); // TODO add assert message assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender),
"An account balance may only be reduced by the holder or a holder-approved agent";
} }
/// This rule should always fail. /// This rule should always fail.