Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University #255

Closed
openjml-project opened this issue Apr 24, 2014 · 16 comments
Closed

URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University #255

openjml-project opened this issue Apr 24, 2014 · 16 comments
Assignees
@davidcok
Labels
bug OpenJML

Comments

@openjml-project
Copy link

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.

Original comment by: keith-foster
@openjml-project
Copy link
Author

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.

Original comment by: davidcok

@openjml-project
Copy link
Author

Another workaround is to make pos an int instead of an Integer.

Original comment by: davidcok

@openjml-project
Copy link
Author

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 08:19 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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

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:

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.

<ListSeq.java>
<Seq.java>
<SeqTest.groovy>

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 08:19 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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

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.

  • David

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 08:19 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/

[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/

Original comment by: davidcok

@openjml-project
Copy link
Author

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:

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.

David
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 08:19 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/

[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/

[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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

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:

From: Keith Foster keith.foster@rmit.edu.au
Subject: Re: [jmlspecs:bugs] #402 URGENT: JML rac "Internal Bug please report" preventing my teaching JML at RMIT University
Date: 26 April 2014 3:41:59 pm AEST
To: "[jmlspecs:bugs]" 402@bugs.jmlspecs.p.re.sf.net

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:

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.

<ListSeq.java>
<Seq.java>
<SeqTest.groovy>

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 08:19 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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

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 and ArrayList 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).

    5. 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.

    Original comment by: davidcok

@openjml-project
Copy link
Author

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:

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 and ArrayList 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.

[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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

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

Original comment by: davidcok

@openjml-project
Copy link
Author

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

Original comment by: davidcok

@openjml-project
Copy link
Author

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.

  • David

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/

Original comment by: davidcok

@openjml-project
Copy link
Author

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.

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.

David
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/

[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/

Original comment by: keith-foster

@openjml-project
Copy link
Author

Excellent. I'm glad it went well. And I have some things to fix (once I get the SMTCOMP organized :-).

  • David

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.

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 Option for TAB_SIZE in jmlunit #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.
    David
    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: Parse level 0 (static) data groups #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:Parse level 0 (static) data groups #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/
    [bugs:Parse level 0 (static) data groups #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/

[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/

Original comment by: davidcok

@openjml-project
Copy link
Author

  • labels: --> OpenJML
  • Module: none --> OpenJML

Original comment by: davidcok

@davidcok
Copy link
Member

This example compiles OK in current OpenJML - see sf402 in racfiles. Closing the issue

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@davidcok davidcok

Labels
bug OpenJML
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@davidcok @openjml-project