junit in JML 5.5 behaving strangely
|
View:
New views
8 Messages
—
Rating Filter:
Alert me
|
 |
junit in JML 5.5 behaving strangely
by Joseph Kiniry
::
Rate this Message:
Hi all,
I am attempting to re-run some old extensive unit tests in JML 5.5. Hundreds of my tests are failing with traces akin to: Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid Expression in "<GENERATED-BY-mjc>", line 0, character 0 JMLEvaluationError cause: class org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError Anyone recognize this offhand? Joe ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Patrice Chalin-3
::
Rate this Message:
Can you send the details of one of the tests that is failing? It seems
that there is a runtime error being raised during the evaluation of an assertion (recall that definedness checking is now the default). Joseph Kiniry wrote: > Hi all, > > I am attempting to re-run some old extensive unit tests in JML 5.5. > Hundreds of my tests are failing with traces akin to: > > Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid > Expression in "<GENERATED-BY-mjc>", line 0, character 0 > JMLEvaluationError cause: class > org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError > > Anyone recognize this offhand? > > Joe > Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof. Dependable Software Research Group, CSE Department, Concordia University Room EV3.215, Phone +1-514-848-2424 x3004. www.encs.concordia.ca/~chalin ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Joseph Kiniry
::
Rate this Message:
On 15 Jul, 2008, at 18:37, Patrice Chalin wrote: > Can you send the details of one of the tests that is failing? It > seems that there is a runtime error being raised during the > evaluation of an assertion (recall that definedness checking is now > the default). Hrm. E.g., in the KOA tally system, AuditLog's class initializer is failing. Unfortunately, none of its invariants are under-defined. https://trac.ucd.ie/trac/browser/software/evoting/koa/trunk/plugins/DutchTallySystem/src/sos/koa/AuditLog.java The bogus instance invariant on the field kiesKringen has been removed in my sandbox. Joe > Joseph Kiniry wrote: >> Hi all, >> >> I am attempting to re-run some old extensive unit tests in JML >> 5.5. Hundreds of my tests are failing with traces akin to: >> >> Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid >> Expression in "<GENERATED-BY-mjc>", line 0, character 0 >> JMLEvaluationError cause: class >> org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError >> >> Anyone recognize this offhand? >> >> Joe ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Joseph Kiniry
::
Rate this Message:
Patrice et al,
On 15 Jul, 2008, at 18:37, Patrice Chalin wrote: > Can you send the details of one of the tests that is failing? It > seems that there is a runtime error being raised during the > evaluation of an assertion (recall that definedness checking is now > the default). After further investigation with both jProfiler and the Eclipse debugger, I'm guessing that the problem is perhaps related to an interaction between the new definedness checking and JML-junit. I suspect that JML-junit has not being upgraded to support the new default behavior of programs compiled with jmlc, because as far as I recall, there are no jml-junit system tests in JML4. Are the old assertion semantics completely gone from JML >= 5.5? I see no command-line switch to trigger old behavior. I am struggling with this new behavior in the general. E.g., when I attempt to run the tally application within jmlrac 5.5 I see failures as well in class initializers for classes that have no invariants. I am now reinstalling JML 5.4 and 5.3 to test against those releases. I can provide a workspace snapshot, of course, for others to have a look at. It is over 150MB when uncompressed through, as it is the full KOA workspace. Joe > Joseph Kiniry wrote: >> Hi all, >> >> I am attempting to re-run some old extensive unit tests in JML >> 5.5. Hundreds of my tests are failing with traces akin to: >> >> Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid >> Expression in "<GENERATED-BY-mjc>", line 0, character 0 >> JMLEvaluationError cause: class >> org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError >> >> Anyone recognize this offhand? >> >> Joe ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Patrice Chalin-3
::
Rate this Message:
Joseph Kiniry wrote:
Patrice et al,Right, I do not recall any updates being made to jmlunit. Are the old assertion semantics completely gone from JML >= 5.5? I see no command-line switch to trigger old behavior.Here is the usage help I get with CVS head: usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files>The option you want is --oldSemantics. I suspect that these should also be the options of the 5.5 release. I'll try to find time to download KOA and try it out though it will likely not be before tomorrow (Thursday). Cheers, Patrice -- Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof. Dependable Software Research Group, CSE Department, Concordia University Room EV3.215, Phone +1-514-848-2424 x3004. www.encs.concordia.ca/~chalin ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Joseph Kiniry
::
Rate this Message:
Hi Patrice,
On 16 Jul, 2008, at 13:58, Patrice Chalin wrote: > Joseph Kiniry wrote: >> >> Patrice et al, >> >> On 15 Jul, 2008, at 18:37, Patrice Chalin wrote: >> >>> Can you send the details of one of the tests that is failing? It >>> seems that there is a runtime error being raised during the >>> evaluation of an assertion (recall that definedness checking is >>> now the default). >> >> After further investigation with both jProfiler and the Eclipse >> debugger, I'm guessing that the problem is perhaps related to an >> interaction between the new definedness checking and JML-junit. I >> suspect that JML-junit has not being upgraded to support the new >> default behavior of programs compiled with jmlc, because as far as >> I recall, there are no jml-junit system tests in JML4. > Right, I do not recall any updates being made to jmlunit. Ok. FYI, running our unit tests in JML 5.4 results in error messages that make sense, so something changed from 5.4 to 5.5 that is breaking jml- junit. >> Are the old assertion semantics completely gone from JML >= 5.5? I >> see no command-line switch to trigger old behavior. > Here is the usage help I get with CVS head: > usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files> > > Options: > --Assignable, -A: Check that a method with an assignable clause does > not call methods that do not have an assignable clause [true] > --Quiet, -Q: Shuts off all typechecking informational messages [false] > ... > --oldSemantics, -O: use old expression translation mecanism that > emulates 2-valued logic [false] The option you want is -- > oldSemantics. I suspect that these should also be the options of > the 5.5 release. Ah, I was looking at the jml man page, forgetting that jmlc includes the extra switches for compilation. It looks like the new non-null defaults are also biting me, as our specs were assuming nullable references. Unfortunately, as ESC/Java2 still does not support nullable_by_default, it looks like I'll have to update the spec of every reference in the system. :( For the moment I'll just try to put in nullable_by_default and not use ESC/Java2. > I'll try to find time to download KOA and try it out though it will > likely not be before tomorrow (Thursday). No problem. I'll perhaps have solved local problems by then, but someone should really look at updating jml-junit for the new jmlc behavior. Joe ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: junit in JML 5.5 behaving strangely
by Perry James-3
::
Rate this Message:
Hi Joe,
Can't you revert to nullable by default with jmlc's -n switch? --defaultNonNull, -n: Make reference paramenters, fields and method return types non_null by default [true] Perry On Wed, Jul 16, 2008 at 9:18 AM, Joseph Kiniry <kiniry@...> wrote:
------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: jml-unit, and esc/java2 with non-null by default
by Patrice Chalin-3
::
Rate this Message:
Joseph Kiniry wrote:
> It looks like the new non-null defaults are also biting me, as our > specs were assuming nullable references. Unfortunately, as ESC/Java2 > still does not support nullable_by_default, it looks like I'll have to > update the spec of every reference in the system. :( > > For the moment I'll just try to put in nullable_by_default and not use > ESC/Java2. FYI, while I don't plan on implementing support for the {non_null,nullable}_by_default modifiers in esc2, I'm almost done with adding support for the -nonNullByDefault command line argument (the new default works for method return types and parameters). >> I'll try to find time to download KOA and try it out though it will >> likely not be before tomorrow (Thursday). > No problem. I'll perhaps have solved local problems by then, but > someone should really look at updating jml-junit for the new jmlc > behavior. I agree, though we should try to work towards a jmlunit for jml4. Cheers, Patrice -- Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof. Dependable Software Research Group, CSE Department, Concordia University Room EV3.215, Phone +1-514-848-2424 x3004. www.encs.concordia.ca/~chalin ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
| Free Forum Powered by Nabble | Forum Help |