diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index c976a27bec1674a24e830ba13ce2dec1547352ea..4e3f05dbabff7e8c023675ea80d637f893a73ef8 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.1.qualifier
+Bundle-Version: 3.4.0.qualifier
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Export-Package: org.eventb.core.ast,
@@ -18,7 +18,8 @@ Export-Package: org.eventb.core.ast,
org.eventb.internal.core.parser.operators;x-friends:="org.eventb.core.ast.tests",
org.eventb.internal.core.typecheck;x-friends:="org.eventb.core.ast.tests"
Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.6
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Bundle-Activator: org.eventb.internal.core.ast.ASTPlugin
Require-Bundle: org.eclipse.core.runtime
Eclipse-ExtensibleAPI: true
+Automatic-Module-Name: org.eventb.core.ast
diff --git a/build.gradle b/build.gradle
index ec9b263ba664f2bffb9deeeff9ddba0a014b21de..88b96deed276cbc11ed4d298f4b6e520bfd384cc 100644
--- a/build.gradle
+++ b/build.gradle
@@ -6,7 +6,7 @@ plugins {
}
project.group = 'de.hhu.stups'
-project.version = "3.4.0"
+project.version = "3.5.0-SNAPSHOT"
final isSnapshot = project.version.endsWith("-SNAPSHOT")
sourceSets {
@@ -37,7 +37,7 @@ task tom() {
}
java {
- sourceCompatibility = JavaVersion.VERSION_1_7
+ sourceCompatibility = JavaVersion.VERSION_1_8
withSourcesJar()
withJavadocJar()
diff --git a/src/org/eventb/core/ast/Formula.java b/src/org/eventb/core/ast/Formula.java
index 39fbe60477274319e9de415457b687de98f64430..37ab2f7b1584ae8c6513868c8cf4f879fe5204e1 100644
--- a/src/org/eventb/core/ast/Formula.java
+++ b/src/org/eventb/core/ast/Formula.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2017 ETH Zurich and others.
+ * Copyright (c) 2005, 2018 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
@@ -988,6 +988,7 @@ public abstract class Formula<T extends Formula<T>> {
return result;
}
+ @SafeVarargs
private static <S extends Formula<?>> ArrayList<FreeIdentifier[]> getFreeIdentifiers(
S... formulas) {
final ArrayList<FreeIdentifier[]> lists = new ArrayList<FreeIdentifier[]>(
@@ -1008,6 +1009,7 @@ public abstract class Formula<T extends Formula<T>> {
* @return a sorted merged array of identifiers or <code>null</code> if an
* error occurred
*/
+ @SafeVarargs
protected static <S extends Formula<?>> IdentListMerger mergeFreeIdentifiers(
S... formulas) {
diff --git a/src/org/eventb/core/ast/FormulaFactory.java b/src/org/eventb/core/ast/FormulaFactory.java
index f6f0a9ce5f5131af10d0f8453f3682704db504bf..6a4488a1061073fbcd6e1bde34b24e687cd33bda 100644
--- a/src/org/eventb/core/ast/FormulaFactory.java
+++ b/src/org/eventb/core/ast/FormulaFactory.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2015 ETH Zurich and others.
+ * Copyright (c) 2005, 2018 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
@@ -2067,6 +2067,9 @@ public class FormulaFactory {
* if the given string doesn't denote a formula position
*/
public static IPosition makePosition(String image) {
+ if (image.length() == 0) {
+ return IPosition.ROOT;
+ }
return new Position(image);
}
diff --git a/src/org/eventb/core/ast/IAccumulator.java b/src/org/eventb/core/ast/IAccumulator.java
index 3f3e4beba2f284e74d62518d9174ffc23e7cdf5e..518e906440d107658bbf277dd99806c027057b7d 100644
--- a/src/org/eventb/core/ast/IAccumulator.java
+++ b/src/org/eventb/core/ast/IAccumulator.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2011 Systerel and others.
+ * Copyright (c) 2010, 2018 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
@@ -76,6 +76,7 @@ public interface IAccumulator<F> {
* @param findings
* findings to accumulate
*/
+ @SuppressWarnings("unchecked") // Actually safe in the single implementation
void add(F... findings);
/**
diff --git a/src/org/eventb/core/ast/ISealedTypeEnvironment.java b/src/org/eventb/core/ast/ISealedTypeEnvironment.java
index b80bcfada33df5d4e015bea5c990e13b4729d35d..cfaf545a5b11e5af15659c6840ec4619345b4885 100644
--- a/src/org/eventb/core/ast/ISealedTypeEnvironment.java
+++ b/src/org/eventb/core/ast/ISealedTypeEnvironment.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2012 Systerel and others.
+ * Copyright (c) 2012, 2018 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
@@ -19,6 +19,8 @@ package org.eventb.core.ast;
* </p>
*
* @since 3.0
+ * @noextend This interface is not intended to be extended by clients.
+ * @noimplement This interface is not intended to be implemented by clients.
*/
public interface ISealedTypeEnvironment extends ITypeEnvironment {
diff --git a/src/org/eventb/core/ast/extension/ITypeCheckMediator.java b/src/org/eventb/core/ast/extension/ITypeCheckMediator.java
index 08a8bcf4f5796e8f62421de047181982e4b2a8c8..ad2ea6f690b8759b99fae2784bccfc50969ab813 100644
--- a/src/org/eventb/core/ast/extension/ITypeCheckMediator.java
+++ b/src/org/eventb/core/ast/extension/ITypeCheckMediator.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2013 Systerel and others.
+ * Copyright (c) 2010, 2018 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
@@ -17,6 +17,7 @@ import org.eventb.core.ast.Type;
*
* @author Nicolas Beauger
* @since 2.0
+ * @noextend This interface is not intended to be extended by clients.
* @noimplement This interface is not intended to be implemented by clients.
*/
public interface ITypeCheckMediator extends ITypeMediator {
diff --git a/src/org/eventb/internal/core/ast/FindingAccumulator.java b/src/org/eventb/internal/core/ast/FindingAccumulator.java
index 9ea2d3e0ddb7bf97fd1c424d2ec33e1254ef92b4..99e10290274f7a7d131f0ae839d411445e20c3e6 100644
--- a/src/org/eventb/internal/core/ast/FindingAccumulator.java
+++ b/src/org/eventb/internal/core/ast/FindingAccumulator.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2011 Systerel and others.
+ * Copyright (c) 2010, 2018 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
@@ -77,7 +77,8 @@ public class FindingAccumulator<F> implements IAccumulator<F> {
}
@Override
- public void add(F... items) {
+ @SafeVarargs
+ public final void add(F... items) {
for (F item : items) {
findings.add(item);
}
diff --git a/src/org/eventb/internal/core/ast/Position.java b/src/org/eventb/internal/core/ast/Position.java
index 755631b1304104c13806620ee7e3bc9665034c32..96e060c8613c7dcea6bd1339fb181fa099647230 100644
--- a/src/org/eventb/internal/core/ast/Position.java
+++ b/src/org/eventb/internal/core/ast/Position.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2006, 2011 ETH Zurich and others.
+ * Copyright (c) 2006, 2018 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
@@ -26,19 +26,13 @@ import org.eventb.core.ast.IPosition;
public final class Position implements IPosition {
public static IPosition getRoot() {
- return new Position();
+ return new Position(new int[0]);
}
- private static final int[] NO_INTS = new int[0];
-
private static final Pattern DOT_PATTERN = Pattern.compile("\\.");
public final int[] indexes;
- private Position() {
- this.indexes = NO_INTS;
- }
-
private Position(int[] indexes) {
this.indexes = indexes;
}
@@ -48,24 +42,19 @@ public final class Position implements IPosition {
}
public Position(String image) {
- if (image.length() == 0) {
- this.indexes = NO_INTS;
- } else {
- final String[] components = DOT_PATTERN.split(image, -1);
- final int length = components.length;
- this.indexes = new int[length];
- for (int i = 0; i < length; i++) {
- try {
- final int idx = Integer.parseInt(components[i]);
- if (idx < 0) {
- throw new IllegalArgumentException(
- "Negative index in position: " + image);
- }
- this.indexes[i] = idx;
- } catch (NumberFormatException e) {
- throw new IllegalArgumentException("Invalid position: "
- + image);
+ final String[] components = DOT_PATTERN.split(image, -1);
+ final int length = components.length;
+ this.indexes = new int[length];
+ for (int i = 0; i < length; i++) {
+ try {
+ final int idx = Integer.parseInt(components[i]);
+ if (idx < 0) {
+ throw new IllegalArgumentException(
+ "Negative index in position: " + image);
}
+ this.indexes[i] = idx;
+ } catch (NumberFormatException e) {
+ throw new IllegalArgumentException("Invalid position: " + image);
}
}
}
diff --git a/src/org/eventb/internal/core/parser/BMath.java b/src/org/eventb/internal/core/parser/BMath.java
index 0214c6d2be3882e1c371df462b6be702f3f03cce..781efa225606c71216053cb01762afaa650dc4e2 100644
--- a/src/org/eventb/internal/core/parser/BMath.java
+++ b/src/org/eventb/internal/core/parser/BMath.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2013 Systerel and others.
+ * Copyright (c) 2010, 2019 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
@@ -170,9 +170,11 @@ public abstract class BMath extends AbstractGrammar {
addCompatibility(MUL_ID, MOD_ID);
addAssociativity(MUL_ID);
addCompatibility(DIV_ID, MUL_ID);
+ addCompatibility(DIV_ID, DIV_ID);
addCompatibility(DIV_ID, MOD_ID);
- addCompatibility(MOD_ID, DIV_ID);
addCompatibility(MOD_ID, MUL_ID);
+ addCompatibility(MOD_ID, DIV_ID);
+ addCompatibility(MOD_ID, MOD_ID);
addCompatibility(NEG_LIT.getImage(), PLUS_ID);
addCompatibility(NEG_LIT.getImage(), MINUS_ID);