#121 Support for inner classes

[shanleyr]

JML Version: JML.5.0_rc2

Running code with jmlrac (and compiled with jmlc): After
the point where an anonymous instance of an inner
interface is passed to a method, the checker no longer
works properly.

The next "ensures" expression in the example does not
cause an exception to be raised when it should be!

The problem only happens when both of the following
conditions are satisfied:

1) The interface is defined within the class.
2) An anonymous instance is created.

See the attached code for an example.

[shanleyr]

Example code showing bug in JML impl

[Yoonsik Cheon]

Logged In: YES
user_id=636250

Hi, thanks for your bug report. Nested or inner classes are
not supported by jmlc yet, so I will move this bug report to
the feature request.

[shanleyr]

Logged In: YES
user_id=1096684

Hi,

I'm not sure if I explained this properly (because I still think
this is a bug and not a feature request).

The key point is perhaps that the "ensures" is in no way
related to the inner class. So IMHO, just because inner
classes are not supported does not mean the checker should
stop working for supported features.

By the way, I encountered this behaviour when writing
contracts on a class that indirectly used one of our standard
API classes that used the mentioned pattern. It took me a
long time to track down what the actual cause was.