From 855a975d65479fd1ddb2b98994a94ca57a9bf28d Mon Sep 17 00:00:00 2001
From: ellab123 <ellab@microsoft.com>
Date: Wed, 22 Apr 2020 16:24:36 -0700
Subject: [PATCH] new test for VeriSol.Modifies; VeriSolContracts.sol extended
 for Modifies

---
 Test/config/Modifies.json                     |  6 +++
 Test/records.txt                              |  1 +
 .../Libraries/VeriSolContracts.sol            | 22 ++++++++
 Test/regressions/Modifies.sol                 | 52 +++++++++++++++++++
 4 files changed, 81 insertions(+)
 create mode 100644 Test/config/Modifies.json
 create mode 100644 Test/regressions/Modifies.sol

diff --git a/Test/config/Modifies.json b/Test/config/Modifies.json
new file mode 100644
index 00000000..53338443
--- /dev/null
+++ b/Test/config/Modifies.json
@@ -0,0 +1,6 @@
+{
+    "recursionBound": 8,
+    "k": 1,
+    "main": "CorralEntry_Test",
+    "expectedResult": "Program has no bugs"
+}
diff --git a/Test/records.txt b/Test/records.txt
index 4e6cea9d..0810145e 100644
--- a/Test/records.txt
+++ b/Test/records.txt
@@ -206,3 +206,4 @@ FuncsWithUnnamedParams.sol
 transfer.sol
 ownable.sol
 calldata.sol
+Modifies.sol
diff --git a/Test/regressions/Libraries/VeriSolContracts.sol b/Test/regressions/Libraries/VeriSolContracts.sol
index 181d0715..1d05d190 100644
--- a/Test/regressions/Libraries/VeriSolContracts.sol
+++ b/Test/regressions/Libraries/VeriSolContracts.sol
@@ -100,5 +100,27 @@ library VeriSol {
     function Modifies(mapping (address => uint256) storage a, address[8] memory x) public pure;
     function Modifies(mapping (address => uint256) storage a, address[9] memory x) public pure;
     function Modifies(mapping (address => uint256) storage a, address[10] memory x) public pure;
+	
+	function Modifies(mapping (address => int256) storage a, address[1] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[2] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[3] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[4] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[5] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[6] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[7] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[8] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[9] memory x) public pure;
+    function Modifies(mapping (address => int256) storage a, address[10] memory x) public pure;
+	
+	function Modifies(mapping (address => bool) storage a, address[1] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[2] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[3] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[4] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[5] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[6] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[7] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[8] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[9] memory x) public pure;
+	function Modifies(mapping (address => bool) storage a, address[10] memory x) public pure;
 
 }
\ No newline at end of file
diff --git a/Test/regressions/Modifies.sol b/Test/regressions/Modifies.sol
new file mode 100644
index 00000000..49429471
--- /dev/null
+++ b/Test/regressions/Modifies.sol
@@ -0,0 +1,52 @@
+pragma solidity ^0.5.0;
+
+// Tests different types of mappings as arguments for VeriSol.Modifies
+
+import "SafeMath.sol";
+import "./Libraries/VeriSolContracts.sol";
+
+contract Test {
+	using SafeMath for uint256;
+	
+	mapping (address => uint256) public mapUint256;
+	mapping (address => int256) public mapInt256;
+	mapping (address => bool) public mapBool;
+	
+	constructor() public {}
+	
+	function modUint256(address a, address b) public {
+		mapUint256[a] = mapUint256[a] + 3;
+		mapUint256[b] = mapUint256[b] + 5;
+	}
+	
+	function modUint256Wrapper(address a, address b) public {
+		modUint256(a, b);
+		VeriSol.Modifies(mapUint256, [a, b]);
+		//VeriSol.Modifies(mapUint256, [a]);     //fails
+		//VeriSol.Modifies(mapUint256, [b]);     //fails  
+	}
+	
+	function modInt256(address a, address b, int256 amount) public {	
+		mapInt256[a] = mapInt256[a] + amount;
+		mapInt256[b] = mapInt256[b] - amount;
+	}
+	
+	function modInt256Wrapper(address a, address b, int256 amount) public {
+		modInt256(a, b, amount);
+		VeriSol.Modifies(mapInt256, [a, b]);
+		//VeriSol.Modifies(mapInt256, [a]);        //fails
+		//VeriSol.Modifies(mapInt256, [b]);        //fails
+	}
+	
+	function modBool(address a, address b) public {	
+		mapBool[a] = !mapBool[a];
+		mapBool[b] = !mapBool[b];
+	}
+	
+	function modBoolWrapper(address a, address b) public {
+		modBool(a, b);
+		VeriSol.Modifies(mapBool, [a, b]);
+		VeriSol.Modifies(mapBool, [a]);     //TODO: passes b/c of the bug
+		VeriSol.Modifies(mapBool, [b]);     //TODO: passes b/c of the bug
+	}
+}
\ No newline at end of file