From 2a75aa19bdc79ab67921ba63984f2840f761ba7a Mon Sep 17 00:00:00 2001 From: Michael George Date: Thu, 9 Dec 2021 17:17:49 -0500 Subject: [PATCH] added munging to scripts --- certora/scripts/Governor.sh | 2 ++ certora/scripts/GovernorCountingSimple-counting.sh | 4 +++- certora/scripts/WizardControlFirstPriority.sh | 4 +++- certora/scripts/WizardFirstTry.sh | 2 ++ certora/scripts/sanity.sh | 4 +++- certora/scripts/verifyAll.sh | 2 ++ 6 files changed, 15 insertions(+), 3 deletions(-) diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh index 7b44e364a..53ade5060 100755 --- a/certora/scripts/Governor.sh +++ b/certora/scripts/Governor.sh @@ -1,3 +1,5 @@ +make -C certora munged + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ --verify GovernorHarness:certora/specs/GovernorBase.spec \ --solc solc8.0 \ diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh index 82b2c263e..9ed8fe34c 100644 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ b/certora/scripts/GovernorCountingSimple-counting.sh @@ -1,3 +1,5 @@ +make -C certora munged + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ @@ -5,4 +7,4 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBa --optimistic_loop \ --settings -copyLoopUnroll=4 \ --rule hasVotedCorrelation \ - --msg "$1" \ No newline at end of file + --msg "$1" diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh index 3f367de2c..b815986ee 100644 --- a/certora/scripts/WizardControlFirstPriority.sh +++ b/certora/scripts/WizardControlFirstPriority.sh @@ -1,3 +1,5 @@ +make -C certora munged + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ --link WizardControlFirstPriority:token=ERC20VotesHarness \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ @@ -7,4 +9,4 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardContr --optimistic_loop \ --settings -copyLoopUnroll=4 \ --rule canVoteDuringVotingPeriod \ - --msg "$1" \ No newline at end of file + --msg "$1" diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/WizardFirstTry.sh index 361814d8b..fd5a32ab4 100644 --- a/certora/scripts/WizardFirstTry.sh +++ b/certora/scripts/WizardFirstTry.sh @@ -1,3 +1,5 @@ +make -C certora munged + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ --verify WizardFirstTry:certora/specs/GovernorBase.spec \ --solc solc8.2 \ diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh index 58b27cc7d..b6cdb4ec3 100644 --- a/certora/scripts/sanity.sh +++ b/certora/scripts/sanity.sh @@ -1,3 +1,5 @@ +make -C certora munged + for f in certora/harnesses/Wizard*.sol do echo "Processing $f" @@ -9,4 +11,4 @@ do --optimistic_loop \ --msg "checking sanity on ${file%.*}" --settings -copyLoopUnroll=4 -done \ No newline at end of file +done diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh index f55ab8abf..90d76912c 100644 --- a/certora/scripts/verifyAll.sh +++ b/certora/scripts/verifyAll.sh @@ -1,5 +1,7 @@ #!/bin/bash +make -C certora munged + for contract in certora/harnesses/Wizard*.sol; do for spec in certora/specs/*.spec;