Issue 61: Plural should know that this != null
Status:  Fixed
Owner:
Closed:  Mar 2009
Project Member Reported by jonathan...@cs.cmu.edu, Mar 7, 2009
What steps will reproduce the problem?
1. define method A without a precondition "this != null"
2. pass this to a method B that has the precondition "#0 != null"

What is the expected output? What do you see instead?

I expect this to pass, because this != null is an invariant of Java 
semantics.  But Plural complains that it can't prove that this != null.  

What version of the product are you using? On what operating system?

Plural 1.0.6, Crystal 3.3.7, Eclipse 3.4.1 on Windows XP


Mar 13, 2009
Project Member #1 kevin.bi...@gmail.com
Test case in r238; fix in r239
Status: Fixed
Owner: kevin.bierhoff