search

microsoft / verisol

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

Verisol fails on call with non-empty argument #196

Open bmarwritescode opened 4 years ago

bmarwritescode commented 4 years ago

Summary

When trying to use the call function with any non-empty arguments (i.e. anything not ""), Verisol throws an error.

Minimal Example

contract CallError {

  function errorTest(bytes memory data) public {
    address nameReg = 0x72bA7d8E73Fe8Eb666Ea66babC8116a41bFb10e2;
    bool success;
    bytes memory returnData;
    (success, returnData) = address(nameReg).call(data);
    require(success);
  }

}

I run this example with the following command:

dotnet Binaries/VeriSol.dll ./CallError.sol CallError /omitAxioms /omitSourceLineInfo /omitUnsignedSemantics /omitDataValuesInTrace

And get the following error:

VeriSol translation error: File , Line -1, Contract CallError, Function errorTest:: low-level call statements with non-empty signature not implemented......

If you replace address(nameReg).call(data) with address(nameReg).call("");, Verisol does not throw any error.

shuvendu-lahiri commented 4 years ago

This is expected as seen from the error message. I will add it as an enhancement instead of a bug, as VeriSol has tried to consciously stay away from low-level calls. We supported call("") as it is a common method for sending ether with adjustable gas budget.