search

microsoft / verisol

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

Adding type "bytesK"; new test for "using" bug in a library #226

Closed ellab123 closed 4 years ago

ellab123 commented 4 years ago

Test TwoLibraries.sol fails to compile:

VeriSol translation error: File C:\VeriSol-10-07\verisol\Test\regressions\TwoLibraries.sol, Line 5, Contract Counters, Function decrement:: Unknown type of internal function call: counter._value.sub....

The bug is that IsLibraryFunctionCall method does not account for the case when "using" is located inside a library.

shuvendu-lahiri commented 4 years ago

@ellab123 can you add a test to exercise various byteN types and add other byteN types in the code?

shuvendu-lahiri commented 4 years ago

Quick question: did you mean to add BytesTypes.sol to the regression? Is there a test to check your bytes related changes.