microsoft / verisol

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

Scientific Notation not Supported #235

Open stephensj2 opened 4 years ago

stephensj2 commented 4 years ago

Solidity allows users to express large numbers in scientific notation like so: x = 2.5e1; Such an assignment is relatively common in tokens as they make specifying large numbers such as the token limit easy. However, when VeriSol tries to translate such a value, it throws the following error: VeriSol translation error: The value could not be parsed.

It would be useful if VeriSol could identify the value that caused the translation error if this construct was difficult to support. A test case is given below.

test.txt