microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Add modifies clauses #220

Open shuvendu-lahiri opened 4 years ago

shuvendu-lahiri commented 4 years ago

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 commented 4 years ago

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
    }
}