How to handle methods called from constructor?

[Eddie Aftandilian]

Hi,

I'm seeing this error when I attempt to call an instance method from a constructor:

Foo.java:123: error: call to initHelper() not allowed on the given receiver.
    initHelper();
                       ^
  found   : @UnderInitialization(com.google.Bar.class) @NonNull MyClass
  required: @Initialized @NonNull MyClass

How should I tell the initialization checker that it is OK to call that method even though the object is not yet initialized?

Thanks,

Eddie

[Michael Ernst]

Eddie-

(As background for anyone reading this who doesn't know what a method
receiver is, see
http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#faq-receiver
.)

You are getting the error because you have a call like

x.myMethod(y, z)

but the receiver argument x is not compatible with the method declaration.

At the declaration of myMethod, you can state the requirements on the
type of each formal parameter. You can annotate the receiver formal
parameter of a method in the same way as you annotate any other formal
parameter.

By default, each formal parameter is implicitly annotated as
@Initialized. The receiver parameter is always named "this", and you
are allowed to omit it if you are just accepting the default
annotation.

Suppose that myMethod doesn't depend on the receiver being fully
initialized; in other words, it's OK to call x.myMethod(y, z) even if
x is not initialized. Here is how you would do that:

class MyClass {

int myMethod(@UnknownInitialization MyClass this, String param1, boolean param2) { ... }

}

If you are using annotations in comments, you would write:

class MyClass {

int myMethod(/*>>>@UnknownInitialization MyClass this,*/ String param1, boolean param2) { ... }

}

-Mike

[Eddie Aftandilian]

Thanks, Mike.  A follow up question: let's say I have a class that looks like this:

public class Foo {

  private Object field1;

  private Object field2;

  public Foo() {

    field1 = new Object();

    initHelper();

    field2 = new Object();

  }

  public void initHelper(@UnknownInitialization Foo this) {

    field1.toString();

  }

}

In this case I get an error that the call to field1.toString() is a dereference of a possibly null field field1.  Is the correct thing to do to annotate initHelper() with @RequiresNonNull("field1")?

Thanks,

Eddie

[Michael Ernst]

Eddie-

Yes, adding
@RequiresNonNull("field1")
is exactly the right thing to do in this case.

-Mike


> Subject: Re: How to handle methods called from constructor?
> From: Eddie Aftandilian <eaf...@google.com>
> To: Michael Ernst <mer...@cs.washington.edu>
> Date: Thu, 26 Sep 2013 14:18:00 -0700

[Eddie Aftandilian]

Another question: Is there a way to suppress errors related only to initialization?  We were previously using "-AsuppressWarnings=initialization", but that seems to turn off most of the nullness checking.  For example, this obvious nullness violation isn't caught when you pass that option:

public class Repro {

  private Object obj;

  public Repro() {

    obj = new Object();

  }

  public void foo() {

    obj = null;  // BUG: assigning null to @Nonnull ref

  }

}

[Werner Dietl]

The following changeset should fix this:

https://code.google.com/p/checker-framework/source/detail?r=453cf23a8f31

Please let me know whether this works for you.
cu, WMD.

> --
>
> ---
> You received this message because you are subscribed to the Google Groups
> "Checker Framework discussion" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to checker-framework-...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.



--
http://www.google.com/profiles/wdietl