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

did some harnessing

Browse Source
This commit is contained in:
Michael George
2021-12-02 16:47:18 -05:00
parent 5888bee853
commit d64869545d
2 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
certora/scripts/WizardFirstTry.sh
View File

@ -3,6 +3,6 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirst
--solc solc8.2 \
--staging shelly/forSasha \
--optimistic_loop \
--disableLocalTypeChecking \
--settings -copyLoopUnroll=4 \
--rule allFunctionsRevertIfCanceled \
--msg "$1"
--msg "$1"

8
certora/specs/GovernorBase.spec
View File

@ -25,8 +25,8 @@ methods {
getVotes(address, uint256) returns uint256 => DISPATCHER(true)
erc20votes.getPastTotalSupply(uint256) returns uint256
erc20votes.getPastVotes(address, uint256) returns uint256
getPastTotalSupply(uint256) returns uint256 => NONDET
getPastVotes(address, uint256) returns uint256 => NONDET
//scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
//executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
@ -281,7 +281,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f ->
&& f.selector != updateTimelock(address).selector
&& f.selector != updateQuorumNumerator(uint256).selector
&& f.selector != queue(address[],uint256[],bytes[],bytes32).selector
&& f.selector != __acceptAdmin().selector
&& f.selector != 0xb9a61961 // __acceptAdmin()
} {
env e; calldataarg args;
uint256 pId;
@ -302,7 +302,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered {
&& f.selector != updateTimelock(address).selector
&& f.selector != updateQuorumNumerator(uint256).selector
&& f.selector != queue(address[],uint256[],bytes[],bytes32).selector
&& f.selector != __acceptAdmin().selector
&& f.selector != 0xb9a61961 // __acceptAdmin()
} {
env e; calldataarg args;
uint256 pId;