Bug 422796

Description Patrice Chalin 2013-11-28 13:32:25 EST

Consider the code given below. Note the spurious potential NPE reported at (*).

import org.jmlspecs.annotation.NonNullByDefault;
import org.jmlspecs.annotation.Nullable;
import org.junit.Test;

@NonNullByDefault
public class NullExprTest {
	
	private @Nullable Boolean b() { return null; }
	
	@Test
	public void testBoolean() {
		Boolean b1 = b();
		boolean b = b1 == null || 
				b1; // <-- reports potential NPE (*)
		org.junit.Assert.assertTrue(b);
	}

}