The range of MethodDeclaration does not include the range of JmlContracts. Range invariant `child.range \subseteq child.parent.range` should be adhered.
The range of MethodDeclaration does not include the range of JmlContracts.
Range invariant
child.range \subseteq child.parent.rangeshould be adhered.