Add modifies clauses

[shuvendu-lahiri]

No description provided.

[shuvendu-lahiri]

One issue with the current prototype is that the line number for the violation of a modifies is always the last statement of the function, as it is installed as a postcondition in Boogie.

[shuvendu-lahiri]

Support modifies clause for Boolean maps and nested maps.

import "./Libraries/VeriSolContracts.sol";

contract Test {
	mapping (address => bool) public mapBool;
	
	constructor() public {}
	
	function modBool(address a, address b) public {	
                mapBool[a] = true;
                mapBool[b] = true;
		VeriSol.Modifies(mapBool, [a, b]); // should pass
		VeriSol.Modifies(mapBool, [a]);     // should fail
		VeriSol.Modifies(mapBool, [b]);     // should fail
	}
}