Armada's concrete-level checker doesn't prevent return statements that access multiple shared locations, such as return s where s is an addressable struct.
The proper fix is probably to just disallow arguments in return statements. One should return values by assigning them to output parameters, then using a bare return statement.
Armada's concrete-level checker doesn't prevent return statements that access multiple shared locations, such as return s where s is an addressable struct.
The proper fix is probably to just disallow arguments in return statements. One should return values by assigning them to output parameters, then using a bare return statement.