diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF index 91b52c6f29b63443593290086346a65fa1abbba3..c976a27bec1674a24e830ba13ce2dec1547352ea 100644 --- a/META-INF/MANIFEST.MF +++ b/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: %pluginName Bundle-SymbolicName: org.eventb.core.ast;singleton:=true -Bundle-Version: 3.3.0.qualifier +Bundle-Version: 3.3.1.qualifier Bundle-Vendor: %providerName Bundle-Localization: plugin Export-Package: org.eventb.core.ast, diff --git a/build.gradle b/build.gradle index be2473c521400bb20667321de2dfc5926ef2449c..972371688bc4908ac7d4ca4536a833411b21a1bd 100644 --- a/build.gradle +++ b/build.gradle @@ -6,7 +6,7 @@ plugins { } project.group = 'de.hhu.stups' -project.version = "3.3.0" +project.version = "3.4.0-SNAPSHOT" final isSnapshot = project.version.endsWith("-SNAPSHOT") sourceSets { diff --git a/src/org/eventb/core/ast/BecomesMemberOf.java b/src/org/eventb/core/ast/BecomesMemberOf.java index e555f6ad7c366d9189984fbfdee0ae5b84cac8c5..6b088495de0a632755e88b7c8f27581b6ea9e24f 100644 --- a/src/org/eventb/core/ast/BecomesMemberOf.java +++ b/src/org/eventb/core/ast/BecomesMemberOf.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -228,7 +228,7 @@ public class BecomesMemberOf extends Assignment { goOn = visitor.continueBECOMES_MEMBER_OF(this); } if (goOn) { - goOn = setExpr.accept(visitor); + setExpr.accept(visitor); } return visitor.exitBECOMES_MEMBER_OF(this); } diff --git a/src/org/eventb/core/ast/BecomesSuchThat.java b/src/org/eventb/core/ast/BecomesSuchThat.java index 4aadea9a7337ccaec33197a9ff0da94205bbcbbe..9837c24c4bbff59fafeda8789f21ddc8d8782e31 100644 --- a/src/org/eventb/core/ast/BecomesSuchThat.java +++ b/src/org/eventb/core/ast/BecomesSuchThat.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -293,7 +293,7 @@ public class BecomesSuchThat extends Assignment { } if (goOn) { - goOn = condition.accept(visitor); + condition.accept(visitor); } return visitor.exitBECOMES_SUCH_THAT(this); diff --git a/src/org/eventb/core/ast/BinaryExpression.java b/src/org/eventb/core/ast/BinaryExpression.java index ed8c2a0d3f2f165fb3afbb8fac2fa3b647b6dfb6..6ead4e960c01661cd090ee5630c4b40d54fe73ae 100644 --- a/src/org/eventb/core/ast/BinaryExpression.java +++ b/src/org/eventb/core/ast/BinaryExpression.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -731,7 +731,7 @@ public class BinaryExpression extends Expression { } } - if (goOn) goOn = right.accept(visitor); + if (goOn) right.accept(visitor); switch (getTag()) { case MAPSTO: return visitor.exitMAPSTO(this); diff --git a/src/org/eventb/core/ast/BinaryPredicate.java b/src/org/eventb/core/ast/BinaryPredicate.java index f5e51922129c692166c2112c4162dd703bee3fcd..39a35b4045477b37e066aa2b14614424a1471658 100644 --- a/src/org/eventb/core/ast/BinaryPredicate.java +++ b/src/org/eventb/core/ast/BinaryPredicate.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -265,7 +265,7 @@ public class BinaryPredicate extends Predicate { } } - if (goOn) goOn = right.accept(visitor); + if (goOn) right.accept(visitor); switch (getTag()) { case LIMP: return visitor.exitLIMP(this); diff --git a/src/org/eventb/core/ast/BoolExpression.java b/src/org/eventb/core/ast/BoolExpression.java index 528a61a81473812f96d88ae38cc7cc2e59f4d9a4..3ea4fbd496bb817188e33a21c731fcea74da45b7 100644 --- a/src/org/eventb/core/ast/BoolExpression.java +++ b/src/org/eventb/core/ast/BoolExpression.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -216,7 +216,7 @@ public class BoolExpression extends Expression { default: assert false; } - if (goOn) goOn = child.accept(visitor); + if (goOn) child.accept(visitor); switch (getTag()) { case KBOOL: return visitor.exitKBOOL(this); diff --git a/src/org/eventb/core/ast/ISpecialization.java b/src/org/eventb/core/ast/ISpecialization.java index b89d27fa179086517238884850464aeca773a990..977019472782cfe6d90755a16df18cd6b2a29e02 100644 --- a/src/org/eventb/core/ast/ISpecialization.java +++ b/src/org/eventb/core/ast/ISpecialization.java @@ -94,7 +94,7 @@ package org.eventb.core.ast; * @noimplement This interface is not intended to be implemented by clients. * @since 2.6 */ -public interface ISpecialization { +public interface ISpecialization extends Cloneable { /** * Returns a deep copy of this specialization. This method is useful to diff --git a/src/org/eventb/core/ast/QuantifiedExpression.java b/src/org/eventb/core/ast/QuantifiedExpression.java index 41b178fb2d5271b820d65ebc9f3a22f115bffc6c..9f5dccfaae4d19e7ce41f29004c49af01d68359c 100644 --- a/src/org/eventb/core/ast/QuantifiedExpression.java +++ b/src/org/eventb/core/ast/QuantifiedExpression.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2014 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -655,7 +655,7 @@ public class QuantifiedExpression extends Expression { } if (goOn) goOn = pred.accept(visitor); if (goOn) goOn = acceptContinue(visitor); - if (goOn) goOn = expr.accept(visitor); + if (goOn) expr.accept(visitor); switch (getTag()) { case QUNION: return visitor.exitQUNION(this); diff --git a/src/org/eventb/core/ast/QuantifiedPredicate.java b/src/org/eventb/core/ast/QuantifiedPredicate.java index 161fc412d9b620bb6148729d15dd6118c8ca4347..4551beb8e86846ef813792db960cc8fce2f4bbcc 100644 --- a/src/org/eventb/core/ast/QuantifiedPredicate.java +++ b/src/org/eventb/core/ast/QuantifiedPredicate.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2014 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -352,7 +352,7 @@ public class QuantifiedPredicate extends Predicate { } } } - if (goOn) goOn = pred.accept(visitor); + if (goOn) pred.accept(visitor); switch (getTag()) { case FORALL: return visitor.exitFORALL(this); diff --git a/src/org/eventb/core/ast/RelationalPredicate.java b/src/org/eventb/core/ast/RelationalPredicate.java index fcb442dd94cfcc14f1caac195d03b3d15acedfa1..3b7b6f61fb695db979b2ddb17e62aacb1bc0e46d 100644 --- a/src/org/eventb/core/ast/RelationalPredicate.java +++ b/src/org/eventb/core/ast/RelationalPredicate.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -378,7 +378,7 @@ public class RelationalPredicate extends Predicate { } } - if (goOn) goOn = right.accept(visitor); + if (goOn) right.accept(visitor); switch (getTag()) { case EQUAL: return visitor.exitEQUAL(this); diff --git a/src/org/eventb/core/ast/SimplePredicate.java b/src/org/eventb/core/ast/SimplePredicate.java index 72fd385cebf0f0c3d68e3f7356a41dc54bdbc5e2..8474f65ba5ee17921cf21801b70f3df9034bfc4a 100644 --- a/src/org/eventb/core/ast/SimplePredicate.java +++ b/src/org/eventb/core/ast/SimplePredicate.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -228,7 +228,7 @@ public class SimplePredicate extends Predicate { default: assert false; } - if (goOn) goOn = child.accept(visitor); + if (goOn) child.accept(visitor); switch (getTag()) { case KFINITE: return visitor.exitKFINITE(this); diff --git a/src/org/eventb/core/ast/UnaryExpression.java b/src/org/eventb/core/ast/UnaryExpression.java index 329ee5b7e638443a5c92bb4d35c81a24dc21c0ec..17fdebbd004927cf1dfbfa501ac48820d639225a 100644 --- a/src/org/eventb/core/ast/UnaryExpression.java +++ b/src/org/eventb/core/ast/UnaryExpression.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -528,7 +528,7 @@ public class UnaryExpression extends Expression { default: assert false; } - if (goOn) goOn = child.accept(visitor); + if (goOn) child.accept(visitor); switch (getTag()) { case KCARD: return visitor.exitKCARD(this); diff --git a/src/org/eventb/core/ast/UnaryPredicate.java b/src/org/eventb/core/ast/UnaryPredicate.java index d6aee4e95c9f3a013c8b9de9a7f6e218ef40499c..129000f46d7f62a6a0823b44b03e2f4b0bfa1e66 100644 --- a/src/org/eventb/core/ast/UnaryPredicate.java +++ b/src/org/eventb/core/ast/UnaryPredicate.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2013 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -222,7 +222,7 @@ public class UnaryPredicate extends Predicate { default: assert false; } - if (goOn) goOn = child.accept(visitor); + if (goOn) child.accept(visitor); switch (getTag()) { case NOT: return visitor.exitNOT(this); diff --git a/src/org/eventb/internal/core/ast/FreshNameSolver.java b/src/org/eventb/internal/core/ast/FreshNameSolver.java index 39467cac1ef2d1b5dde961ff60b32e2497b3d0da..06f060058ca61e749ddb73744324049440c933fa 100644 --- a/src/org/eventb/internal/core/ast/FreshNameSolver.java +++ b/src/org/eventb/internal/core/ast/FreshNameSolver.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2005, 2012 ETH Zurich and others. + * Copyright (c) 2005, 2017 ETH Zurich and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -155,7 +155,7 @@ public class FreshNameSolver { prefix = matcher.group(1); final String digits = matcher.group(2); if (digits.length() != 0) - suffix = Integer.valueOf(digits); + suffix = Integer.parseInt(digits); else suffix = -1; quotes = matcher.group(3); @@ -174,4 +174,4 @@ public class FreshNameSolver { } } -} \ No newline at end of file +} diff --git a/src/org/eventb/internal/core/ast/TypeTranslatabilityChecker.java b/src/org/eventb/internal/core/ast/TypeTranslatabilityChecker.java index 530dd65c3b8085b2951d2f9da53b9229e381b41e..848c5d277e1076dbaf21a03c927588989bec8f77 100644 --- a/src/org/eventb/internal/core/ast/TypeTranslatabilityChecker.java +++ b/src/org/eventb/internal/core/ast/TypeTranslatabilityChecker.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2013 Systerel and others. + * Copyright (c) 2013, 2017 Systerel and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -72,7 +72,7 @@ public class TypeTranslatabilityChecker implements ITypeVisitor { @Override public void visit(GivenType type) { - isTranslatable &= target.isValidIdentifierName(type.getName()); + isTranslatable = isTranslatable && target.isValidIdentifierName(type.getName()); } @Override @@ -82,7 +82,7 @@ public class TypeTranslatabilityChecker implements ITypeVisitor { @Override public void visit(ParametricType type) { - isTranslatable &= target.hasExtension(type.getExprExtension()); + isTranslatable = isTranslatable && target.hasExtension(type.getExprExtension()); for (Type child : type.getTypeParameters()) { child.accept(this); } @@ -99,4 +99,4 @@ public class TypeTranslatabilityChecker implements ITypeVisitor { type.getRight().accept(this); } -} \ No newline at end of file +} diff --git a/src/org/eventb/internal/core/ast/wd/Lemma.java b/src/org/eventb/internal/core/ast/wd/Lemma.java index bc820faddb886244d67ca71523b3c36ec01ca347..1db4d33b2a7c3e8d5df913732d4de8cb93564c07 100644 --- a/src/org/eventb/internal/core/ast/wd/Lemma.java +++ b/src/org/eventb/internal/core/ast/wd/Lemma.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2010, 2012 Systerel and others. + * Copyright (c) 2010, 2017 Systerel and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -40,6 +40,8 @@ public class Lemma { */ @Override public boolean equals(Object obj) { + if (obj == null) + return false; if (this == obj) return true; @@ -117,4 +119,4 @@ public class Lemma { set.add(this); } -} \ No newline at end of file +} diff --git a/src/org/eventb/internal/core/parser/MainParsers.java b/src/org/eventb/internal/core/parser/MainParsers.java index c7d9eac0990a745e963f22e344184613af0b1d8d..ef2aa08bdabc5fbd1d22aa3b1b7f9058a78e6a0c 100644 --- a/src/org/eventb/internal/core/parser/MainParsers.java +++ b/src/org/eventb/internal/core/parser/MainParsers.java @@ -1,5 +1,5 @@ /******************************************************************************* - * Copyright (c) 2010, 2013 Systerel and others. + * Copyright (c) 2010, 2017 Systerel and others. * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 * which accompanies this distribution, and is available at @@ -138,10 +138,6 @@ public class MainParsers { // errors must be non empty protected static ASTProblem newCompoundError(SourceLocation loc, Set<ASTProblem> errors) { - final List<String> messages = new ArrayList<String>(errors.size()); - for (ASTProblem astProblem : errors) { - messages.add(astProblem.toString()); - } return new ASTProblem(loc, ProblemKind.VariousPossibleErrors, ProblemSeverities.Error, ProblemKind.makeCompoundMessage(errors));