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