Experimental options in VeriSol - microsoft/verisol GitHub Wiki

In this page, we describe some of the options that are not exercised by default.

Assuming VeriSol.exe is in your path. Change current directory to Test\regressions folder.

Modeling unknown fallback functions as callbacks

The following example illustrates a specification that is violated in the presence of reentrancy. The /stubModel:callback uses a model of the environment where a fallback function of an unknown dynamic type can call back into any of the public methods of the caller.

VeriSol.exe DAO-demo.sol SimpleDAO /stubModel:callback

Once fixed (comment out the line with // bug and uncomment the line with // fix), the example shows the use of postconditions (using VeriSol.Ensures clause) for recursive methods to perform compositional proofs.

Modular arithmetic

The ERC20 OpenZeppelin implementation optimizes the check for enough balance in _transfer through the use of SafeMath.sol. The following example shows a specification (a contract invariant that uses SumMapping function) that breaks when SafeMath is not used (needs /useModularArithmetic flag.

VeriSol.exe ERC20-demo.sol ERC20 /useModularArithmetic	

Once fixed (comment the line with // bug and uncomment the next line), the contract should verify.

Scalable counterexample finding for AssetTransfer

The following example shows that the default bound on the number of transactions considered for finding a specification violation may not suffice, and the bound may need to be increased by supplying /txBound.

VeriSol.exe A__AssetTransfer_Workbench.sol AssetTransferWrper /txBound:7