microsoft / verisol

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

Type Modifier Translation Error #237

Closed stephensj2 closed 4 years ago

stephensj2 commented 4 years ago

It appears that annotating variable types with required modifiers such as payable affect VeriSol's ability to find functions. When trying to translate the function transferOwnership in the file given below, VeriSol fails with the following message:

VeriSol translation error: File , Line -1, Contract Ownable, Function transferOwnership:: Cannot find a function with signature: _transferOwnership(address)

The specified function does appear in the file, however it has type _transferOwnership(address payable). It should be noted that the variable used to call _transferOwnership is also of type address payable.

Ownable.txt

shuvendu-lahiri commented 4 years ago

closing.