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

finilized rules

Browse Source
This commit is contained in:
Aleksander Kryukov
2022-04-08 15:38:26 +01:00
parent da674eced1
commit 75417fbf9f
6 changed files with 246 additions and 255 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
certora/specs/AccessControl.spec
View File

@ -11,7 +11,7 @@ methods {
// STATUS - verified
// check onlyRole modifier for grantRole()
// If `onlyRole` modifier reverts then `grantRole()` reverts
rule onlyRoleModifierCheckGrant(env e){
bytes32 role; address account;
@ -58,7 +58,7 @@ rule grantRoleEffect(env e){
// STATUS - verified
// grantRole() does not affect another accounts
// revokeRole() does not affect another accounts
rule revokeRoleEffect(env e){
bytes32 role; address account;
bytes32 anotherRole; address nonEffectedAcc;