From d41ed09f133daa8a7b501a087c49f81d39ff335f Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 6 Oct 2023 12:56:07 +0200
Subject: [PATCH] Update to Rodin 3.4 sources
---
META-INF/MANIFEST.MF | 2 +-
build.gradle | 2 +-
src/org/eventb/core/ast/BecomesMemberOf.java | 4 ++--
src/org/eventb/core/ast/BecomesSuchThat.java | 4 ++--
src/org/eventb/core/ast/BinaryExpression.java | 4 ++--
src/org/eventb/core/ast/BinaryPredicate.java | 4 ++--
src/org/eventb/core/ast/BoolExpression.java | 4 ++--
src/org/eventb/core/ast/ISpecialization.java | 2 +-
src/org/eventb/core/ast/QuantifiedExpression.java | 4 ++--
src/org/eventb/core/ast/QuantifiedPredicate.java | 4 ++--
src/org/eventb/core/ast/RelationalPredicate.java | 4 ++--
src/org/eventb/core/ast/SimplePredicate.java | 4 ++--
src/org/eventb/core/ast/UnaryExpression.java | 4 ++--
src/org/eventb/core/ast/UnaryPredicate.java | 4 ++--
src/org/eventb/internal/core/ast/FreshNameSolver.java | 6 +++---
.../internal/core/ast/TypeTranslatabilityChecker.java | 8 ++++----
src/org/eventb/internal/core/ast/wd/Lemma.java | 6 ++++--
src/org/eventb/internal/core/parser/MainParsers.java | 6 +-----
18 files changed, 37 insertions(+), 39 deletions(-)
diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 91b52c6..c976a27 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 be2473c..9723716 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 e555f6a..6b08849 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 4aadea9..9837c24 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 ed8c2a0..6ead4e9 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 f5e5192..39a35b4 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 528a61a..3ea4fbd 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 b89d27f..9770194 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 41b178f..9f5dccf 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 161fc41..4551beb 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 fcb442d..3b7b6f6 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 72fd385..8474f65 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 329ee5b..17fdebb 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 d6aee4e..129000f 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 39467ca..06f0600 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 530dd65..848c5d2 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 bc820fa..1db4d33 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 c7d9eac..ef2aa08 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));
--
GitLab