Menu
▾
▴
3 Attachments
#402 URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
I am compiling a simple demo with JML annotations and I get an internal error :
java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Internal JML bug - please report. BuildOpenJML-20131218-REV3178
java.lang.ArrayIndexOutOfBoundsException: 277
(see full error text attached)
Also find the two source files attached.
I'm working on this promptly. In the meantime, note that the problem relates to using generics (whose implementation is in progress). If you can I suggest you use an example without generic types until this problem is repaired.
Another workaround is to make pos an int instead of an Integer.
Hi David
I have removed all generics and changed boxed types to their primitive counterparts.
The IndexOutOfBounds exception has gone and now the java files are compile into class files (this is good progress) but I still get the following errors saying assertions are not implemented and indeed no assertions are run when I run my test cases which trigger contract violations.
See the command below and the files attached.
w8097129:openjml keith$ java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:54: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:54: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
Please let men know what I’m doing wrong.
Cheers
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 25 Apr 2014, at 7:44 am, David Cok davidcok@users.sf.net wrote:
Related
Bugs: #402
Hi David
Actually I was running a non-intrumented version of the classes in IntelliJ IDEA which did its own compiling without JML instrumentation) and located the class files in a different place. This explains why no assertions happened.
I am now running everything on the command line and have converted the test class from groovy to plain java and JUnit 4.11. However, the test code hangs (on the “.E.E.E.”) every time a JML instrumented method is called. See the command history below (and latest files attached) :
w8097129:openjml keith$ java -jar openjml.jar -command rac -racCompileToJavaAssert ListSeq.java Seq.java
ListSeq.java:51: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:51: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
w8097129:openjml keith$ javac -cp .:junit-4.11.jar SeqTest.java
w8097129:openjml keith$ java -cp .:junit-4.11.jar:hamcrest-core-1.3.jar:jmlruntime.jar org.junit.runner.JUnitCore SeqTest
JUnit version 4.11
.E.E.E.
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 26 Apr 2014, at 2:05 pm, Keith Foster keith.foster@rmit.edu.au wrote:
Related
Bugs: #402
Keith - I see your following email, but to comment on this one:
The messages "
Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression" are benign - they just say that a particular quantified expression is not being tested at runtime. The point I'll note is that it is not obvious which expression that is. If necessary you can always rewrite it as nested quantifiers: e.g. (\forall T o; ...; (\forall T oo; ...))
instead of (\forall T o,oo; ... )
Eventually I will fix this case.
From: Keith keith-foster@users.sf.net
To: [jmlspecs:bugs] 402@bugs.jmlspecs.p.re.sf.net
Sent: Saturday, April 26, 2014 12:36 AM
Subject: [jmlspecs:bugs] Re: #402 URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Hi David
I have removed all generics and changed boxed types to their primitive counterparts.
The IndexOutOfBounds exception has gone and now the java files are compile into class files (this is good progress) but I still get the following errors saying assertions are not implemented and indeed no assertions are run when I run my test cases which trigger contract violations.
See the command below and the files attached.
w8097129:openjml keith$ java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:54: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:54: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
Please let men know what I’m doing wrong.
Cheers
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 25 Apr 2014, at 7:44 am, David Cok davidcok@users.sf.net wrote:
Another workaround is to make pos an int instead of an Integer.
[bugs:#402] URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Status: open
Created: Thu Apr 24, 2014 12:19 PM UTC by Keith
Last Updated: Thu Apr 24, 2014 09:44 PM UTC
Owner: nobody
I am compiling a simple demo with JML annotations and I get an internal error :
java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Internal JML bug - please report. BuildOpenJML-20131218-REV3178
java.lang.ArrayIndexOutOfBoundsException: 277
(see full error text attached)
Also find the two source files attached.
Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/jmlspecs/bugs/402/
To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/
Related
Bugs: #402
note: I’m not using any quantified expressions.
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 27 Apr 2014, at 2:52 am, David Cok davidcok@users.sf.net wrote:
Related
Bugs: #402
forwarded email with java test case
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
Begin forwarded message:
Related
Bugs: #402
Keith,
I created a standalone test harness that calls your tests. I think the following will get you working for your class, while I fix the missing checks you exposed, run the test suite and publish a current updated version (which will take a few days).
-David
Try the following:
1) Annotate length() with //@ pure helper.
The infinite loop you are seeing is because on a call to length(), OpenJML tests to be sure the invariant is satisfied, but the invariant calls length(). In some situations this recursive situation is detected and warned about, but obviously not here, perhaps because of being called from a non-instrumented test harness.
2) Do the RAC compile using -no-internalSpecs . That will skip any library specifications which have two problems here: (a) the library specs refer to ghost fields that are not present in the default copy of the Java system libraries and (b) it avoids warning about the quantified specs in the library.
3) In ListSeq, make the references to List and ArrayList List<Object> and ArrayList<Object> respectively. The issue I referred to earlier is compililng classes that have generic type parameters themselves. Any uses of generic classes ought to have concrete type parameters.
4) Be sure to run the instrumented program with jmlruntime.jar on the classpath (you probably already are).
These are the commands I'm running:
java -jar openjml.jar -no-internalSpecs -rac Seq.java ListSeq.java
javac -cp . SeqTest.java
java -cp ".;jmlruntime.jar" SeqTest
For good measure I'm attaching the files that work for me, both with the current unstable version and the released version.
Hi David
Thank you. I have overcome the previous problems and I have triggerred some runtime contract violations.
However, It appears ensures with \result is ignored. See the test for pos(). It should trigger a violation of the ensures but does not.
I am attaching the three files cleaned up and with headings prated for each test case.
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 27 Apr 2014, at 6:03 pm, David Cok davidcok@users.sf.net wrote:
Related
Bugs: #402
Keith,
I'm not seeing why testPos() should trigger a postcondition error.
After the call to forth, list.pos() is 2 which is <= 2 and is <= length()
- David
On second thought I see you meant testViolationPos.
It is actually the precondition test that is silently ignored.
Since the precondition is false, the ensures are not evaluated.
You will see it if you compile the test framework with RAC.
Keith, I should have explained a bit more.
A method is permitted to assume that it is called with its preconditions holding. It is the caller's job to be sure that they do. Since SeqTest was not compiled with RAC, it did not check or report the precondition failure.
There are two options:
1) compile SeqTest with RAC as I said in the last note.
2) compile ListSeq (and Seq) with the option -racCheckAssumptions. With this option, RAC checks the precondition assumption at the start of ListSeq as if it were an assertion, and you will also see a report of the precondition violation.
It is reasonable to think that option #2 should be the default, to avoid surprises like this one. If it is the default, then every pre and post condition is by the caller and by the callee, if they are both compiled with RAC. So when both are compiled with RAC, we get double reports of checks and much larger instrumented files (since many more checks are compiled in). In some cases the instrumented files become too big for the compiler. So for now it is not the default, but I see it leads to confusion when working with test drivers. -racCheckAssumptions is your helper here.
From: David Cok davidcok@users.sf.net
To: [jmlspecs:bugs] 402@bugs.jmlspecs.p.re.sf.net
Sent: Sunday, April 27, 2014 9:20 AM
Subject: [jmlspecs:bugs] Re: #402 URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
On second thought I see you meant testViolationPos.
It is actually the precondition test that is silently ignored.
Since the precondition is false, the ensures are not evaluated.
You will see it if you compile the test framework with RAC.
* David
[bugs:#402] URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Status: open
Created: Thu Apr 24, 2014 12:19 PM UTC by Keith
Last Updated: Thu Apr 24, 2014 09:44 PM UTC
Owner: nobody
I am compiling a simple demo with JML annotations and I get an internal error :
java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Internal JML bug - please report. BuildOpenJML-20131218-REV3178
java.lang.ArrayIndexOutOfBoundsException: 277
(see full error text attached)
Also find the two source files attached.
Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/jmlspecs/bugs/402/
To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/
Related
Bugs: #402
Hi David
Thank you very much.
I got a full working example of DbC using JML after your last email.
Our lecture and tutorial on DbC went very well tonight.
Hopefully the students will spread the word on JML.
Cheers and Thanks for your immense help. :-)
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 27 Apr 2014, at 11:33 pm, David Cok davidcok@users.sf.net wrote:
Related
Bugs: #402
Excellent. I'm glad it went well. And I have some things to fix (once I get the SMTCOMP organized :-).
From: Keith keith-foster@users.sf.net
To: [jmlspecs:bugs] 402@bugs.jmlspecs.p.re.sf.net
Sent: Thursday, May 1, 2014 8:01 AM
Subject: [jmlspecs:bugs] Re: #402 URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Hi David
Thank you very much.
I got a full working example of DbC using JML after your last email.
Our lecture and tutorial on DbC went very well tonight.
Hopefully the students will spread the word on JML.
Cheers and Thanks for your immense help. :-)
Keith Foster
Academic (CSIT) and Consulting Senior Software Engineer (ITS)
RMIT University
School of Computer Science and Information Technology
Information Technology Services - Application Delivery - Learning, Teaching and Research
On 27 Apr 2014, at 11:33 pm, David Cok davidcok@users.sf.net wrote:
Keith, I should have explained a bit more.
[bugs:#402] URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Status: open
Created: Thu Apr 24, 2014 12:19 PM UTC by Keith
Last Updated: Thu Apr 24, 2014 09:44 PM UTC
Owner: nobody
I am compiling a simple demo with JML annotations and I get an internal error :
java -jar openjml.jar -rac ListSeq.java Seq.java
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
}
^
Internal JML bug - please report. BuildOpenJML-20131218-REV3178
java.lang.ArrayIndexOutOfBoundsException: 277
(see full error text attached)
Also find the two source files attached.
Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/jmlspecs/bugs/402/
To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/
Related
Bugs: #402