Merge branch 'master' into formal-verification

This commit is contained in:
Hadrien Croubois
2023-02-27 11:00:16 +01:00
515 changed files with 22648 additions and 27910 deletions

View File

@ -1,38 +0,0 @@
#!/usr/bin/env bash
set -euxo pipefail
for contract in certora/harnesses/Wizard*.sol;
do
# NOTE: some spec files are not governor related, and should be run on Wizard*.sol
for spec in certora/specs/*.spec;
do
contractFile=$(basename $contract)
specFile=$(basename $spec)
if [[ "${specFile%.*}" != "RulesInProgress" ]];
then
echo "Processing ${contractFile%.*} with $specFile"
if [[ "${contractFile%.*}" = *"WizardControl"* ]];
then
certoraRun \
certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
--link ${contractFile%.*}:token=ERC20VotesHarness \
--verify ${contractFile%.*}:certora/specs/$specFile "$@" \
--solc solc \
--optimistic_loop \
--disableLocalTypeChecking \
--settings -copyLoopUnroll=4 \
--msg "checking $specFile on ${contractFile%.*}"
else
certoraRun \
certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
--verify ${contractFile%.*}:certora/specs/$specFile "$@" \
--solc solc \
--optimistic_loop \
--disableLocalTypeChecking \
--settings -copyLoopUnroll=4 \
--msg "checking $specFile on ${contractFile%.*}"
fi
fi
done
done

View File

@ -5,7 +5,7 @@ set -euxo pipefail
for f in certora/harnesses/Wizard*.sol
do
echo "Processing $f"
file=$(basename $f)
file="$(basename $f)"
echo ${file%.*}
certoraRun certora/harnesses/$file \
--verify ${file%.*}:certora/specs/sanity.spec "$@" \