In Solidity, when a function can return multiple values it is sometimes desirable to declare new variables to store those values. It is possible to do so by declaring the variables inside a tuple like so:
(uint i, uint j) = fn();
However, such a declaration violates an assertion inside of VeriSol resulting in the following output:
Assertion Failed at SolidityAST.VariableDeclarationStatement.Accept(IASTVisitor visitor) in SolidityAST.cs:line 1274
This error message makes it difficult to understand why the translation failed. It would therefore be helpful if this behavior was either explicitly disallowed (similar to low-level calls), or supported by VeriSol. If the behavior were to be disallowed, the user could easily fix the problem by transforming the above code into:
uint i; uint j; (i, j) = fn();
A simple test case that violates this assertion is provided below.
In Solidity, when a function can return multiple values it is sometimes desirable to declare new variables to store those values. It is possible to do so by declaring the variables inside a tuple like so:
(uint i, uint j) = fn();However, such a declaration violates an assertion inside of VeriSol resulting in the following output:
Assertion Failed at SolidityAST.VariableDeclarationStatement.Accept(IASTVisitor visitor) in SolidityAST.cs:line 1274This error message makes it difficult to understand why the translation failed. It would therefore be helpful if this behavior was either explicitly disallowed (similar to low-level calls), or supported by VeriSol. If the behavior were to be disallowed, the user could easily fix the problem by transforming the above code into:
uint i; uint j; (i, j) = fn();A simple test case that violates this assertion is provided below.
bug1.txt