Function arguments are not mutable

[dddejan]

We now have a type error in boogie to fix:

./solc-verify.py test/libsolidity/syntaxTests/types/rational_number_huge.sol --output .
Error while running verifier, details:
Parsing ./rational_number_huge.sol.bpl
./rational_number_huge.sol.bpl(16,5): Error: command assigns to an immutable variable: y#2
./rational_number_huge.sol.bpl(17,5): Error: command assigns to an immutable variable: y#2
2 type checking errors detected in ./rational_number_huge.sol.bpl

CSL-CAS12299:solidity-sri dejan$ code rational_number_huge.sol.bpl 

Originally posted by @dddejan in https://github.com/SRI-CSL/solidity/issues/5#issuecomment-501428136

[hajduakos]

The issue here is that in Solidity you can assign to function parameters, but in Boogie they are immutable. One way to fix this is to make copies at the beginning of the function. The other is to not support such assignments. In general it is considered as a bad practice, VS code should also give a warning: https://ethereum.stackexchange.com/questions/59128/error-security-no-assign-param-avoid-assigning-to-function-parameters . In the latter case, we could have a more informative error message.

[dddejan]

Can you give a link to why/where it is considered bad practice?

I feel this is pretty arbitrary, and it's quite common to reuse variables in general programming languages.

I would supporting this as long as the compiler doesn't disallow it.

[hajduakos]

There used to be a rule in the default linter for VS code: https://github.com/duaraghav8/solium-plugin-security#list-of-rules, I also remember getting the warning. But now I cannot reproduce it. Seems like they don't have it in the latest version: https://ethlint.readthedocs.io/en/latest/user-guide.html#list-of-style-rules . But I've also seen it in e.g. PMD (for Java): https://pmd.github.io/latest/pmd_rules_java_bestpractices.html#avoidreassigningparameters

But I am not against supporting it.

[dddejan]

This is actually quite common, so I'm marking as a bug.