No PreconditionError if Constructor must use a super(..)

[nhatminhle]

_From erwin_st...@gmx.de on January 11, 2012 05:13:31_

1. I have this class from one of your test classes public class In extends FileInputStream { @Requires("(!name.equals(\"/dev/null\"))") public In(String name) throws FileNotFoundException { super(name); } }
2. in a main method: In in = new In("/dev/null");

Expected: PreconditionError Indeed: FileNotFoundException

Version R139 / Windows XP Please provide any additional information below. 1a. public class In { @Requires("(!name.equals(\"/dev/null\"))") public In(String name) throws FileNotFoundException { } } 2a. in a main method: In in = new In("/dev/null");

Expected: PreconditionError Indeed: PreconditionError

Original issue: http://code.google.com/p/cofoja/issues/detail?id=34

[nhatminhle]

From nhat.min...@gmail.com on January 11, 2012 05:35:55

Thanks for reporting. Unfortunately, this is a known bug (well, at least, known to us) and we have yet to come up with a reasonable work-around (and this particular misfeature had fallen off my radar, to be honest).

The short explanation is that in Java, the super() call comes first in the constructor, and anything we inject in the method comes after it. That is currently enforced by the bytecode instrumentation library we're using (ASM), so maybe we should try to contact the guys working on ASM to see if they know of a way around it.

You might be tempted to think that because of contract inheritance, things could work out, but technically speaking, constructors do not inherit from each other, rather they call each other (i.e. in the form of the super() call).

In any case, there's no quick fix to this one, so please live with it for the time being.

Status: Accepted

[nhatminhle]

From nhat.min...@gmail.com on August 16, 2014 03:31:37

Status: WontFix