From d06d3accd8b08df9462073772aa73c9cf59c03df Mon Sep 17 00:00:00 2001 From: miguelmtzinf Date: Fri, 30 Jul 2021 10:58:37 +0200 Subject: [PATCH] feat: Rename LendingPoolHarnessForVariableDebtToken --- .gitlab-ci.yml | 2 +- runVariableTokenCLI.sh | 2 +- specs/VariableDebtToken.spec | 2 +- ...ariableDebtToken.sol => PoolHarnessForVariableDebtToken.sol} | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) rename specs/harness/{LendingPoolHarnessForVariableDebtToken.sol => PoolHarnessForVariableDebtToken.sol} (98%) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 45329d30e..23de908a6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -61,7 +61,7 @@ certora-test: script: - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc_args "['--optimize']" --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --cloud - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args "['--optimize']" --settings -useBitVectorTheory --cache UserConfiguration --cloud - - certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args "['--optimize']" --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --cloud + - certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/PoolHarnessForVariableDebtToken.sol --solc_args "['--optimize']" --link VariableDebtToken:POOL=PoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --cloud only: - master - merge_requests diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh index 2618d57c9..621376783 100644 --- a/runVariableTokenCLI.sh +++ b/runVariableTokenCLI.sh @@ -1 +1 @@ -certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --cache VariableToken --cloud \ No newline at end of file +certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/PoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=PoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --cache VariableToken --cloud \ No newline at end of file diff --git a/specs/VariableDebtToken.spec b/specs/VariableDebtToken.spec index eb19d1b4f..cb19c8ddb 100644 --- a/specs/VariableDebtToken.spec +++ b/specs/VariableDebtToken.spec @@ -1,4 +1,4 @@ -using LendingPoolHarnessForVariableDebtToken as POOL +using PoolHarnessForVariableDebtToken as POOL /** Checks that each possible opertaion changes the balance of at most one user. diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/PoolHarnessForVariableDebtToken.sol similarity index 98% rename from specs/harness/LendingPoolHarnessForVariableDebtToken.sol rename to specs/harness/PoolHarnessForVariableDebtToken.sol index 02f8fa7ee..c2f11c3d4 100644 --- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol +++ b/specs/harness/PoolHarnessForVariableDebtToken.sol @@ -12,7 +12,7 @@ import {DataTypes} from '../../contracts/protocol/libraries/types/DataTypes.sol' Certora: Harness that delegates calls to the original Pool. Used for the verification of the VariableDebtToken contract. */ -contract LendingPoolHarnessForVariableDebtToken is IPool { +contract PoolHarnessForVariableDebtToken is IPool { Pool private originalPool; function deposit(