From 066b4834d3e8140fddd1d3d7a4aa883ecd3ce528 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 29 Aug 2014 15:06:45 +0200
Subject: [PATCH] fix a few warnings
---
.../disprover/core/DisproverReasoner.java | 27 ++++++++++++++-----
.../core/internal/DisproverIdentifier.java | 6 +----
.../translation/DisproverContextCreator.java | 22 ++++++++++++---
3 files changed, 40 insertions(+), 15 deletions(-)
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
index 1c7f3f8c..08d81201 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
@@ -1,17 +1,31 @@
package de.prob.eventb.disprover.core;
-import java.util.*;
+import java.util.HashSet;
+import java.util.Set;
import org.eclipse.core.runtime.Status;
-import org.eventb.core.*;
+import org.eventb.core.IEventBProject;
+import org.eventb.core.IPOSequent;
import org.eventb.core.ast.Predicate;
-import org.eventb.core.seqprover.*;
+import org.eventb.core.seqprover.IConfidence;
+import org.eventb.core.seqprover.IProofMonitor;
+import org.eventb.core.seqprover.IProofRule;
import org.eventb.core.seqprover.IProofRule.IAntecedent;
-import org.rodinp.core.*;
+import org.eventb.core.seqprover.IProverSequent;
+import org.eventb.core.seqprover.IReasoner;
+import org.eventb.core.seqprover.IReasonerInput;
+import org.eventb.core.seqprover.IReasonerInputReader;
+import org.eventb.core.seqprover.IReasonerInputWriter;
+import org.eventb.core.seqprover.IReasonerOutput;
+import org.eventb.core.seqprover.ProverFactory;
+import org.eventb.core.seqprover.SerializeException;
+import org.rodinp.core.IRodinProject;
+import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
-import de.prob.core.*;
+import de.prob.core.Animator;
+import de.prob.core.PrologException;
import de.prob.eventb.disprover.core.internal.DisproverCommand;
import de.prob.eventb.disprover.core.internal.ICounterExample;
import de.prob.eventb.disprover.core.translation.DisproverContextCreator;
@@ -114,6 +128,7 @@ public class DisproverReasoner implements IReasoner {
return counterExample;
}
+ @SuppressWarnings("unused")
private String predicateToProlog(Predicate pred) {
PrologTermStringOutput pto = new PrologTermStringOutput();
TranslationVisitor v = new TranslationVisitor();
@@ -133,7 +148,7 @@ public class DisproverReasoner implements IReasoner {
Predicate goal = sequent.goal();
IAntecedent ante = ProverFactory.makeAntecedent(goal);
-
+
if (counterExample == null) {
return ProverFactory.reasonerFailure(this, input,
"ProB: Error occurred.");
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
index 00a0ed48..69ec7ed4 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.List;
import org.eventb.core.ast.Expression;
-import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.Type;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -28,13 +27,10 @@ public class DisproverIdentifier {
private final String name;
private final Type type;
- private final FormulaFactory ff;
private final boolean givenSet;
- public DisproverIdentifier(String name, Type type, boolean givenSet,
- FormulaFactory ff) {
+ public DisproverIdentifier(String name, Type type, boolean givenSet) {
this.givenSet = givenSet;
- this.ff = ff;
this.name = name;
this.type = type;
}
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
index dceaec2b..12d68b96 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
@@ -1,12 +1,26 @@
package de.prob.eventb.disprover.core.translation;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
-import org.eventb.core.ast.*;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.ITypeEnvironment.IIterator;
+import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IProverSequent;
-import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.node.AAxiomsContextClause;
+import de.be4.classicalb.core.parser.node.AConstantsContextClause;
+import de.be4.classicalb.core.parser.node.ADeferredSetSet;
+import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.ASetsContextClause;
+import de.be4.classicalb.core.parser.node.PContextClause;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.PSet;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.eventb.disprover.core.internal.DisproverIdentifier;
import de.prob.eventb.translator.internal.TranslationVisitor;
@@ -43,7 +57,7 @@ public class DisproverContextCreator {
DisproverIdentifier id = new DisproverIdentifier(
typeIterator.getName(), typeIterator.getType(),
- typeIterator.isGivenSet(), ff);
+ typeIterator.isGivenSet());
// sets are added to the context, vars to the model
if (id.isGivenSet()) {
--
GitLab