From b101af21cc8a6a3433c7809bf46e81f9d710fa54 Mon Sep 17 00:00:00 2001
From: emilio <emilio@ethlend.io>
Date: Thu, 5 Nov 2020 14:43:39 +0100
Subject: [PATCH] Fixed certora harness

---
 ...LendingPoolHarnessForVariableDebtToken.sol | 33 ++++++++-----------
 1 file changed, 13 insertions(+), 20 deletions(-)

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