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