From 4030d487877f29d5e669b5f4efbfaeaa9db1d96e Mon Sep 17 00:00:00 2001
From: pistiner <59415933+orpistiner@users.noreply.github.com>
Date: Thu, 29 Oct 2020 01:57:15 +0200
Subject: [PATCH] Fixes to run on StableDebtToken contract

---
 contracts/tokenization/StableDebtToken.sol |  2 +-
 specs/StableDebtToken.spec                 | 16 ----------------
 specs/harness/StableDebtTokenHarness.sol   |  3 ---
 3 files changed, 1 insertion(+), 20 deletions(-)

diff --git a/contracts/tokenization/StableDebtToken.sol b/contracts/tokenization/StableDebtToken.sol
index 346d9719..a026cfc9 100644
--- a/contracts/tokenization/StableDebtToken.sol
+++ b/contracts/tokenization/StableDebtToken.sol
@@ -286,7 +286,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
    * @param avgRate the average rate at which calculate the total supply
    * @return The debt balance of the user since the last burn/mint action
    **/
-  function _calcTotalSupply(uint256 avgRate) internal view returns (uint256) {
+  function _calcTotalSupply(uint256 avgRate) internal virtual view returns (uint256) {
     uint256 principalSupply = super.totalSupply();
 
     if (principalSupply == 0) {
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index fba0f8ba..718dcb60 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -2,13 +2,6 @@ methods {
 	getUserLastUpdated(address) returns uint40 envfree
 }
 
-ghost ghostSupply() returns uint256;
-
-hook Sstore (slot 0)[address a] uint256 balance (uint256 old_balance) STORAGE {
-	require old_balance <= ghostSupply();
-	havoc ghostSupply assuming ghostSupply@new() == ghostSupply@old() + (balance - old_balance);
-}
-
 rule integrityTimeStamp(address user, method f) {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
@@ -18,15 +11,6 @@ rule integrityTimeStamp(address user, method f) {
 	assert getUserLastUpdated(user) <= e.block.timestamp;
 }
 
-rule totalSupplyInvariant(method f) {
-	env e;
-	require sinvoke getIncentivesController(e) == 0;
-	require totalSupply(e) == ghostSupply();
-	calldataarg arg;
-	sinvoke f(e, arg);
-	assert totalSupply(e) == ghostSupply();
-}
-
 /**
 TotalSupply is the sum of all users’ balances
 	
diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol
index be2471be..d314f8f0 100644
--- a/specs/harness/StableDebtTokenHarness.sol
+++ b/specs/harness/StableDebtTokenHarness.sol
@@ -1,8 +1,5 @@
 pragma solidity ^0.6.8;
 
-import {Context} from '@openzeppelin/contracts/GSN/Context.sol';
-import {IERC20} from '@openzeppelin/contracts/token/ERC20/IERC20.sol';
-import {SafeMath} from '@openzeppelin/contracts/math/SafeMath.sol';
 import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
 import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';