Code demonstrating my problem with the @EnsureNonNull-annotation of the checkers framework. See stackoverflow question http://stackoverflow.com/q/21308736/814206

Tryout_EnsureNonNull.java

package net.kaspervandenberg.trynullcheck;

import checkers.nullness.quals.AssertNonNullIfNonNull;
import checkers.nullness.quals.EnsuresNonNull;
import checkers.nullness.quals.EnsuresNonNullIf;
import checkers.nullness.quals.NonNull;
import checkers.nullness.quals.Nullable;
import dataflow.quals.Pure;

public class Tryout_EnsureNonNull 
{
	private @Nullable Object field = null;

	private @Nullable Object fieldA = null;
	private @Nullable Object fieldB = null;

	@EnsuresNonNull("field")
	public void setFieldNonNull() {
		field = new Object();
	}

	@SuppressWarnings("nullness")				// Required to avoid error on @EnsuresNonNull
	@EnsuresNonNull("getField()")				// ERROR, the postcondition about 'this.getField()' of this method is not satisfied
	public void setFieldMethodNonNull() {
		field = new Object();
	}
	
	@Pure
	public @Nullable Object getField() {
		return field;
	}
	
	@Pure
	public void nonNullArg(@NonNull Object arg) 
	{
		System.out.println( "in non-null" );
	}
	
    public static void main( String[] args )
    {
		Tryout_EnsureNonNull instance = new Tryout_EnsureNonNull();
		instance.nonNullArg(instance);				// success, as expected:
//		instance.nonNullArg(null);				// gives checker error, "incompatible types in argument", as expected

//		instance.nonNullArg(instance.field);	// gives checker error, "incompatible types in argument", as expected
		instance.setFieldNonNull();
		instance.nonNullArg(instance.field);		// works
		instance.setFieldMethodNonNull();
		instance.nonNullArg(instance.getField());
    }
}