Skip to content

Commit

Permalink
Update Certora command (#101)
Browse files Browse the repository at this point in the history
  • Loading branch information
gbalabasquer authored Mar 7, 2023
1 parent 5423864 commit 33732e2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
all :; FOUNDRY_OPTIMIZER=true FOUNDRY_OPTIMIZER_RUNS=200 forge build --use solc:0.8.14
clean :; forge clean
test :; ./test.sh solc="0.8.14" match="$(match)" block="$(block)" match-test="$(match-test)" match-contract="$(match-contract)"
certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,D3MTestGem=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,D3MTestGem=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol src/tests/stubs/D3MTestPlan.sol src/tests/stubs/D3MTestPool.sol src/tests/stubs/D3MTestGem.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=D3MTestGem --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=180$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,D3MTestGem=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,D3MTestGem=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol src/tests/stubs/D3MTestPlan.sol src/tests/stubs/D3MTestPool.sol src/tests/stubs/D3MTestGem.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=D3MTestGem --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=1200,-solver=z3,-adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
deploy :; ./deploy.sh config="$(config)"
deploy-core :; ./deploy-core.sh

0 comments on commit 33732e2

Please sign in to comment.