Fix warnings (#605)

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Jan 18, 2024 · 24cf37b · 24cf37b
1 parent cb1e1af
commit 24cf37b
Show file tree

Hide file tree

Showing 5 changed files with 3 additions and 10 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/MemoryEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/MemoryEvent.java
@@ -6,7 +6,7 @@
 
 import static com.dat3m.dartagnan.program.Register.*;
 
-public interface MemoryEvent extends Event, RegReader {
+public interface MemoryEvent extends RegReader {
 
     List<MemoryAccess> getMemoryAccesses();
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericMemoryEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericMemoryEvent.java
@@ -11,7 +11,7 @@
     By assigning a distinct tag to instances of this event, one can model abstract memory events like SRCU and hazard pointers.
     In that sense, a GenericMemoryEvent is similar to a Fence that carries an actual address.
  */
-public class GenericMemoryEvent extends AbstractMemoryCoreEvent implements MemoryCoreEvent {
+public class GenericMemoryEvent extends AbstractMemoryCoreEvent {
 
     // This is a name for printing only.
     private final String displayName;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java
@@ -5,14 +5,13 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventVisitor;
 import com.dat3m.dartagnan.program.event.MemoryEvent;
-import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.metadata.MemoryOrder;
 
 import java.util.HashSet;
 import java.util.Objects;
 import java.util.Set;
 
-public interface MemoryCoreEvent extends MemoryEvent, RegReader {
+public interface MemoryCoreEvent extends MemoryEvent {
 
     Expression getAddress();
     void setAddress(Expression address);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java
@@ -22,7 +22,6 @@
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
-import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.Model;
 
 import java.math.BigInteger;
@@ -47,7 +46,6 @@ public class ExecutionModel {
 
     // ============= Model specific  =============
     private Model model;
-    private FormulaManager formulaManager;
     private Filter eventFilter;
     private boolean extractCoherences;
 
@@ -223,7 +221,6 @@ public void initialize(Model model, Filter eventFilter, boolean extractCoherence
         // their capacity in previous iterations and thus we should have less overhead in future populations)
         // However, for all intents and purposes, this serves as a constructor.
         this.model = model;
-        formulaManager = encodingContext.getFormulaManager();
         this.eventFilter = eventFilter;
         this.extractCoherences = extractCoherences;
         extractEventsFromModel();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java
@@ -12,7 +12,6 @@
 import com.dat3m.dartagnan.wmm.utils.Tuple;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
-import org.sosy_lab.common.configuration.Options;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -23,8 +22,6 @@
 import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference;
 import static com.google.common.base.Preconditions.checkArgument;
 
-
-@Options
 public class Acyclic extends Axiom {
 
     private static final Logger logger = LogManager.getLogger(Acyclic.class);