search

kiniry / Mobius

4 stars 8 forks source link

JMLc crashes with Phylum error #594

Open atiti opened 11 years ago

atiti commented 11 years ago

voting:src dcochran$ jmlc -P -source 1.4 -d ../jml-src election.tally ie.lero.evoting.scenarioparsing election/tally/AbstractBallotCounting.java parsing election/tally/Ballot.java parsing election/tally/BallotBox.java parsing election/tally/BallotCounting.java parsing election/tally/Candidate.java parsing election/tally/CandidateStatus.java parsing election/tally/CountStatus.java parsing election/tally/Decision.java parsing election/tally/Election.java parsing election/tally/ElectionStatus.java parsing ie/lero/evoting/scenario/Assert.spec parsing ie/lero/evoting/scenario/CheckRemainingSeatsEventM.java parsing ie/lero/evoting/scenario/CountContinuingCandidatesEventK.java parsing ie/lero/evoting/scenario/ElectRemainingCandidatesEventN.java parsing ie/lero/evoting/scenario/ExclusionEventJ.java parsing ie/lero/evoting/scenario/MoveBallotsEventL.java parsing ie/lero/evoting/scenario/QuotaCalculationEventA.java parsing ie/lero/evoting/scenario/SelectHighestContinuingCandidateEventB.java parsing ie/lero/evoting/scenario/SurplusCalculationEventC.java parsing ie/lero/evoting/scenario/TransfersFromExcludedCandidateEventH.java parsing ie/lero/evoting/scenario/TransfersFromSurplusEventD.java parsing election/tally/AbstractBallotCounting.java-refined parsing election/tally/Ballot.java-refined parsing ../../../../../../usr/local/JML/specs/java/lang/Object.jml parsing ../../../../../../usr/local/JML/specs/java/lang/reflect/Array.refines-spec parsing election/tally/BallotBox.java-refined parsing election/tally/mock/MockBallot.java parsing ../../../../../../usr/local/JML/specs/java/lang/IllegalArgumentException.jml parsing ../../../../../../usr/local/JML/specs/java/lang/RuntimeException.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Exception.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Throwable.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/lang/JMLDataGroup.java parsing ../../../../../../usr/local/JML/specs/java/io/Serializable.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/String.jml parsing ../../../../../../usr/local/JML/specs/java/io/UnsupportedEncodingException.refines-spec parsing ../../../../../../usr/local/JML/specs/java/io/IOException.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/Locale.jml parsing ../../../../../../usr/local/JML/specs/java/util/regex/Pattern.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/Comparator.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/Cloneable.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/regex/Matcher.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/Comparable.spec parsing ../../../../../../usr/local/JML/specs/java/lang/CharSequence.spec parsing ../../../../../../usr/local/JML/specs/java/lang/IndexOutOfBoundsException.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/StringBuffer.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSequence.java parsing ../../../../../../usr/local/JML/specs/java/math/BigInteger.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/Number.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSequenceSpecs.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueType.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLCollection.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLType.java parsing ../../../../../../usr/local/JML/specs/java/lang/Class.jml parsing ../../../../../../usr/local/JML/specs/java/io/InputStream.refines-java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLByte.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLComparable.java parsing ../../../../../../usr/local/JML/specs/java/lang/Package.jml parsing ../../../../../../usr/local/JML/specs/java/net/URL.refines-spec parsing ../../../../../../usr/local/JML/specs/java/io/OutputStream.refines-java parsing ../../../../../../usr/local/JML/specs/java/util/Hashtable.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/Dictionary.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/ClassCastException.jml parsing ../../../../../../usr/local/JML/specs/java/util/Enumeration.spec parsing ../../../../../../usr/local/JML/specs/java/util/Map.spec parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsSet.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLListEqualsNode.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLListException.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLSequenceException.java parsing ../../../../../../usr/local/JML/specs/java/util/Collection.spec parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsBag.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLListValueNode.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLNoSuchElementException.java parsing ../../../../../../usr/local/JML/specs/java/util/NoSuchElementException.jml parsing ../../../../../../usr/local/JML/specs/java/lang/IllegalStateException.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsSequence.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsSequenceEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEnumeration.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectType.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLIterator.java parsing ../../../../../../usr/local/JML/specs/java/util/Iterator.spec parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsBagEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLEqualsSetEnumerator.java parsing ../../../../../../usr/local/JML/specs/java/util/Set.spec parsing ../../../../../../usr/local/JML/specs/java/lang/reflect/Field.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/reflect/AccessibleObject.jml parsing ../../../../../../usr/local/JML/specs/java/lang/reflect/Method.jml parsing ../../../../../../usr/local/JML/specs/java/lang/reflect/Constructor.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Byte.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLTypeException.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueBag.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueBagSpecs.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSet.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSetSpecs.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSetEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueBagEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLValueSequenceEnumerator.java parsing ../../../../../../usr/local/JML/specs/java/lang/StringIndexOutOfBoundsException.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/StackTraceElement.refines-spec parsing ../../../../../../usr/local/JML/specs/java/io/PrintStream.refines-java parsing ../../../../../../usr/local/JML/specs/java/io/FilterOutputStream.jml parsing ../../../../../../usr/local/JML/specs/java/io/PrintWriter.refines-java parsing ../../../../../../usr/local/JML/specs/java/lang/CloneNotSupportedException.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/InterruptedException.refines-spec typechecking election/tally/AbstractBallotCounting.java-refined parsing ../../../../../../usr/local/JML/specs/java/lang/Error.jml parsing ../../../../../../usr/local/JML/specs/java/io/File.refines-java parsing ../../../../../../usr/local/JML/specs/java/net/URI.refines-spec parsing ../../../../../../usr/local/JML/specs/java/lang/Character.jml parsing ../../../../../../usr/local/JML/specs/java/lang/NullPointerException.jml parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectSequence.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLListObjectNode.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectBag.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectSet.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectSetEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectBagEnumerator.java parsing ../../../../../../usr/local/JML/org/jmlspecs/models/JMLObjectSequenceEnumerator.java parsing ../../../../../../usr/local/JML/specs/java/io/DataInput.refines-spec parsing ../../../../../../usr/local/JML/specs/java/security/PublicKey.spec parsing ../../../../../../usr/local/JML/specs/java/security/Key.spec parsing ../../../../../../usr/local/JML/specs/java/util/Date.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/Calendar.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/GregorianCalendar.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/ResourceBundle.jml typechecking election/tally/AbstractBallotCounting.java typechecking election/tally/Ballot.java-refined typechecking election/tally/Ballot.java typechecking election/tally/BallotBox.java-refined typechecking election/tally/BallotBox.java typechecking election/tally/BallotCounting.java typechecking election/tally/Candidate.java typechecking election/tally/CandidateStatus.java typechecking election/tally/CountStatus.java typechecking election/tally/Decision.java typechecking election/tally/Election.java typechecking election/tally/ElectionStatus.java typechecking ie/lero/evoting/scenario/Assert.spec typechecking ie/lero/evoting/scenario/CheckRemainingSeatsEventM.java typechecking ie/lero/evoting/scenario/CountContinuingCandidatesEventK.java typechecking ie/lero/evoting/scenario/ElectRemainingCandidatesEventN.java typechecking ie/lero/evoting/scenario/ExclusionEventJ.java typechecking ie/lero/evoting/scenario/MoveBallotsEventL.java typechecking ie/lero/evoting/scenario/QuotaCalculationEventA.java typechecking ie/lero/evoting/scenario/SelectHighestContinuingCandidateEventB.java typechecking ie/lero/evoting/scenario/SurplusCalculationEventC.java typechecking ie/lero/evoting/scenario/TransfersFromExcludedCandidateEventH.java typechecking ie/lero/evoting/scenario/TransfersFromSurplusEventD.java typechecking ../../../../../../usr/local/JML/specs/java/lang/Object.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Float.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Double.jml parsing ../../../../../../usr/local/JML/specs/java/lang/Integer.jml parsing ../../../../../../usr/local/JML/specs/java/util/List.spec parsing ../../../../../../usr/local/JML/specs/java/util/ListIterator.spec parsing ../../../../../../usr/local/JML/specs/java/util/Observer.spec parsing ../../../../../../usr/local/JML/specs/java/util/Observable.refines-spec parsing ../../../../../../usr/local/JML/specs/java/util/SortedMap.spec parsing ../../../../../../usr/local/JML/specs/java/util/SortedSet.spec File "election/tally/AbstractBallotCounting.java", line 334, character 35 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java-refined", line 469, character 9 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java", line 693, character 9 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java-refined", line 834, character 11 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java-refined", line 700, character 26 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/AbstractBallotCounting.java", line 1194, character 28 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/AbstractBallotCounting.java-refined", line 572, character 26 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java", line 1257, character 28 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/AbstractBallotCounting.java", line 1515, character 32 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/Ballot.java", line 90, character 33 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/BallotBox.java-refined", line 18, character 24 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/Candidate.java", line 32, character 22 warning: Entire clause will be dropped since this quantifier is not executable. File "election/tally/Candidate.java", line 138, character 26 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. File "election/tally/Candidate.java", line 159, character 26 warning: Entire clause will be dropped since Sum or Product JmlSpecQuantifiedExpression is not executable. Exception in thread "main" java.lang.NullPointerException at org.multijava.util.compiler.Phylum.(Phylum.java:47) at org.multijava.mjc.JPhylum.(JPhylum.java:50) at org.multijava.mjc.JExpression.(JExpression.java:51) at org.multijava.mjc.JNameExpression.(JNameExpression.java:76) at org.multijava.mjc.JNameExpression.(JNameExpression.java:57) at org.jmlspecs.jmlrac.TransMethod.genDelegatedMethod(TransMethod.java:971) at org.jmlspecs.jmlrac.TransMethod.genWrapperMethod(TransMethod.java:950) at org.jmlspecs.jmlrac.TransMethod.perform(TransMethod.java:163) at org.jmlspecs.jmlrac.TransClass.translateMethod(TransClass.java:324) at org.jmlspecs.jmlrac.TransType.translateBody(TransType.java:752) at org.jmlspecs.jmlrac.TransClass.translateBody(TransClass.java:231) at org.jmlspecs.jmlrac.TransType.translate(TransType.java:355) at org.jmlspecs.jmlrac.JmlRacGenerator.visitJmlClassDeclaration(JmlRacGenerator.java:155) at org.jmlspecs.checker.JmlClassDeclaration.accept(JmlClassDeclaration.java:198) at org.jmlspecs.jmlrac.JmlRacGenerator.visitJmlCompilationUnit(JmlRacGenerator.java:96) at org.jmlspecs.checker.JmlCompilationUnit.accept(JmlCompilationUnit.java:413) at org.jmlspecs.jmlrac.Main$JmlGenerateAssertionTask.processTree(Main.java:701) at org.multijava.mjc.Main$TreeProcessingTask.execute(Main.java:2296) at org.multijava.mjc.Main.processTaskQueue(Main.java:949) at org.multijava.mjc.Main.runCompilation(Main.java:322) at org.multijava.mjc.Main.run(Main.java:127) at org.jmlspecs.jmlrac.Main.compile(Main.java:80) at org.jmlspecs.jmlrac.Main.main(Main.java:74) voting:src dcochran$ jmlc -P -source 1.4 -d ../jml-src election.tally ie.lero.evoting.scenario

atiti commented 11 years ago

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted