search

microsoft / verisol

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

Conversions between fixed-size byte arrays of different lengths are wrong #234

Open ellab123 opened 4 years ago

ellab123 commented 4 years ago

From Solidity v.0.6.1 doc: If a fixed-size bytes type is explicitly converted to a larger type, it is padded on the right, for example: bytes2 a = 0x1234; bytes4 b = bytes4(a); // b will be 0x12340000

In VeriSol, the value of b is exactly the same as the value of a.

shuvendu-lahiri commented 4 years ago

the test is added as a comment in BytesTypes.sol by Ella.