Refinement of string length after checking startsWith or endsWith is supported, but this check can be hidden in a helper method. Therefore, some annotation on such a method is needed so that the refinement can be done at the call site.
Probably could be solved by EnsuresQualifierIf(LongerThanEq) from #11.
Refinement of string length after checking
startsWith
orendsWith
is supported, but this check can be hidden in a helper method. Therefore, some annotation on such a method is needed so that the refinement can be done at the call site. Probably could be solved byEnsuresQualifierIf(LongerThanEq)
from #11.