microsoft / verisol

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

Unsupported types in function invocation #86

Open garbervetsky opened 5 years ago

garbervetsky commented 5 years ago

When a parameter has type bytes32 the tools produces an exception due to an assertion failure.

at System.Diagnostics.Debug.Assert(Boolean condition, String message, String detailMessage) at SolToBoogie.TransUtils.InferFunctionSignature(TranslatorContext context, FunctionCall node) in C:\Users\diegog\source\repos\verisol\Sources\SolToBoogie\TransUtils.cs:line 257

The assertion is missing the type bytes32.

Something similar happens with int32 and uint32. It might fail with other types as well.

Code snippet that produces the assertion failure.

`pragma solidity ^0.4.24;

contract A { function func(bytes32 data) public { // Do something } function caller (bytes32 data) public { func(data); } }`

shuvendu-lahiri commented 4 years ago

Problem lies in VeriSol needs a cast at the call site to get the type, as the compiler infers the type of 23 as int256.

pragma solidity >=0.4.24 < 0.6.0;
contract A {
   function func(int32 data) public {
       // Do something
   }
/*
   function func(int8 data) public {
       // Do something
   }
*/ 
   function caller () public {
     func(23); // does not work, needs int32(23) 
   }
}