Instadapp/aave-protocol-v2
1
0
Fork 0
mirror of https://github.com/Instadapp/aave-protocol-v2.git synced 2024-07-29 21:47:30 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fixed certora harness

Browse Source
This commit is contained in:
emilio 2020-11-05 14:43:39 +01:00
parent add6cad5c3
commit b101af21cc
1 changed files with 13 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
specs/harness/LendingPoolHarnessForVariableDebtToken.sol
View File

@ -8,6 +8,9 @@ import {UserConfiguration} from '../../contracts/libraries/configuration/UserCon
import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol'; import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol'; import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol'; import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
import {
ILendingPoolAddressesProvider
} from '../../contracts/interfaces/ILendingPoolAddressesProvider.sol';
/* /*
Certora: Harness that delegates calls to the original LendingPool. Certora: Harness that delegates calls to the original LendingPool.
@ -25,26 +28,12 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
originalPool.deposit(asset, amount, onBehalfOf, referralCode); originalPool.deposit(asset, amount, onBehalfOf, referralCode);
} }
function withdraw(address asset, uint256 amount) external override { function withdraw(
originalPool.withdraw(asset, amount);
}
function getBorrowAllowance(
address fromUser,
address toUser,
address asset, address asset,
uint256 interestRateMode uint256 amount,
) external override view returns (uint256) { address to
return originalPool.getBorrowAllowance(fromUser, toUser, asset, interestRateMode);
}
function delegateBorrowAllowance(
address asset,
address user,
uint256 interestRateMode,
uint256 amount
) external override { ) external override {
originalPool.delegateBorrowAllowance(asset, user, interestRateMode, amount); originalPool.withdraw(asset, amount, to);
} }
function borrow( function borrow(
@ -193,12 +182,12 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
address receiver, address receiver,
address[] calldata assets, address[] calldata assets,
uint256[] calldata amounts, uint256[] calldata amounts,
uint256 mode, uint256[] calldata modes,
address onBehalfOf, address onBehalfOf,
bytes calldata params, bytes calldata params,
uint16 referralCode uint16 referralCode
) external override { ) external override {
originalPool.flashLoan(receiver, assets, amounts, mode, onBehalfOf, params, referralCode); originalPool.flashLoan(receiver, assets, amounts, modes, onBehalfOf, params, referralCode);
} }
function finalizeTransfer( function finalizeTransfer(
@ -211,4 +200,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
) external override { ) external override {
originalPool.finalizeTransfer(asset, from, to, amount, balanceFromAfter, balanceToBefore); originalPool.finalizeTransfer(asset, from, to, amount, balanceFromAfter, balanceToBefore);
} }
function getAddressesProvider() external override view returns (ILendingPoolAddressesProvider) {
return originalPool.getAddressesProvider();
}
} }