Contracts.Precondition.Not.Satisfied error for `@RequiresNonNull("#1")` but not for `@NonNull` on formal parameter

[aagarwal1012]

I got the contracts.precondition.not.satisfied error while running the following code:
Link to the code.

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class A {
  
  @NonNull String message = "default string";
  
  @RequiresNonNull("#1")
  void setMessage(String message){
    this.message = message;
  }
  
  void main(){
    A object = new A();
    String mess = "random message";
    object.setMessage(mess.substring(0, mess.length() - 3));
  } 
}

class B {
  
  @NonNull String message = "default string";
  
  void setMessage(@NonNull String message){
    this.message = message;
  }
  
  void main(){
    B object = new B();
    String mess = "random message";
    object.setMessage(mess.substring(0, mess.length() - 3));
  } 
}

The exact error message follows :
I had used the Checker Framework Live Demo webpage to produce the error.

Error: [contracts.precondition.not.satisfied] the called method 'object.setMessage(mess.substring(0, mess.length() - 3))' has a precondition 'mess.substring(0, ?)' that is not satisfied

There is no error in the second version that removes @RequiresNonNull and uses @NonNull instead.

[mernst]

You are right that this is an inconsistency between treatment of the two types of annotations. Thanks for noticing this. This is due to details of the implementation and is unlikely to be fixed in the short term.

In the short term, we can make the Checker Framework issue a warning (not an error) if the user writes @Requires* whose argument is exactly a formal parameter name such as "this" or "#1" or "#3". The Checker Framework gives better diagnostics for those. When we have done so, we will close this issue.