Package-sanity tests for solver package.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@17855 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
bnord01 · Sep 18, 2015 · 30dffc3 · 30dffc3
1 parent 0129fc1
commit 30dffc3
Show file tree

Hide file tree

Showing 12 changed files with 200 additions and 19 deletions.
diff --git a/src/org/sosy_lab/solver/FormulaManagerFactory.java b/src/org/sosy_lab/solver/FormulaManagerFactory.java
@@ -102,7 +102,7 @@ public static enum Solvers {
   public FormulaManagerFactory(Configuration config, LogManager pLogger,
       ShutdownNotifier pShutdownNotifier) throws InvalidConfigurationException {
     config.inject(this);
-    logger = pLogger;
+    logger = checkNotNull(pLogger);
     shutdownNotifier = checkNotNull(pShutdownNotifier);
 
     if (!logAllQueries) {

diff --git a/src/org/sosy_lab/solver/PackageSanityTest.java b/src/org/sosy_lab/solver/PackageSanityTest.java
@@ -0,0 +1,37 @@
+/*
+ *  CPAchecker is a tool for configurable software verification.
+ *  This file is part of CPAchecker.
+ *
+ *  Copyright (C) 2007-2015  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *
+ *  CPAchecker web page:
+ *    http://cpachecker.sosy-lab.org
+ */
+package org.sosy_lab.solver;
+
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.configuration.Configuration;
+
+import com.google.common.testing.AbstractPackageSanityTests;
+
+public class PackageSanityTest extends AbstractPackageSanityTests {
+
+  {
+    setDefault(Configuration.class, Configuration.defaultConfiguration());
+    setDefault(ShutdownNotifier.class, ShutdownNotifier.create());
+  }
+}
diff --git a/src/org/sosy_lab/solver/SolverException.java b/src/org/sosy_lab/solver/SolverException.java
@@ -23,6 +23,7 @@
  */
 package org.sosy_lab.solver;
 
+import javax.annotation.Nullable;
 
 /**
  * Exception that should be used if the SMT solver did something wrong.
@@ -31,11 +32,11 @@ public class SolverException extends Exception {
 
   private static final long serialVersionUID = -1557936144555925180L;
 
-  public SolverException(String msg) {
+  public SolverException(@Nullable String msg) {
     super(msg);
   }
 
-  public SolverException(String msg, Throwable t) {
+  public SolverException(@Nullable String msg, @Nullable Throwable t) {
     super(msg, t);
   }
 }
diff --git a/src/org/sosy_lab/solver/api/PackageSanityTest.java b/src/org/sosy_lab/solver/api/PackageSanityTest.java
@@ -0,0 +1,33 @@
+/*
+ *  CPAchecker is a tool for configurable software verification.
+ *  This file is part of CPAchecker.
+ *
+ *  Copyright (C) 2007-2015  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *
+ *  CPAchecker web page:
+ *    http://cpachecker.sosy-lab.org
+ */
+package org.sosy_lab.solver.api;
+
+import com.google.common.testing.AbstractPackageSanityTests;
+
+public class PackageSanityTest extends AbstractPackageSanityTests {
+
+  {
+    setDistinctValues(FormulaType.class, FormulaType.BooleanType, FormulaType.IntegerType);
+  }
+}
diff --git a/src/org/sosy_lab/solver/basicimpl/AbstractFormula.java b/src/org/sosy_lab/solver/basicimpl/AbstractFormula.java
@@ -24,6 +24,10 @@
 package org.sosy_lab.solver.basicimpl;
 
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
+import javax.annotation.Nullable;
+
 import org.sosy_lab.solver.api.ArrayFormula;
 import org.sosy_lab.solver.api.BitvectorFormula;
 import org.sosy_lab.solver.api.BooleanFormula;
@@ -42,13 +46,11 @@ abstract class AbstractFormula<TFormulaInfo> implements Formula {
   private final TFormulaInfo formulaInfo;
 
   protected AbstractFormula(TFormulaInfo formulaInfo) {
-    assert formulaInfo != null;
-
-    this.formulaInfo = formulaInfo;
+    this.formulaInfo = checkNotNull(formulaInfo);
   }
 
   @Override
-  public boolean equals(Object o) {
+  public boolean equals(@Nullable Object o) {
     if (!(o instanceof AbstractFormula)) { return false; }
     return formulaInfo.equals(((AbstractFormula<?>) o).formulaInfo);
   }
@@ -80,8 +82,8 @@ class ArrayFormulaImpl<TI extends Formula, TE extends Formula, TFormulaInfo>
 
   public ArrayFormulaImpl(TFormulaInfo info, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
     super(info);
-    this.indexType = pIndexType;
-    this.elementType = pElementType;
+    this.indexType = checkNotNull(pIndexType);
+    this.elementType = checkNotNull(pElementType);
   }
 
   public FormulaType<TI> getIndexType() {

diff --git a/src/org/sosy_lab/solver/basicimpl/AbstractUninterpretedFunctionDeclaration.java b/src/org/sosy_lab/solver/basicimpl/AbstractUninterpretedFunctionDeclaration.java
@@ -27,6 +27,8 @@
 
 import java.util.List;
 
+import javax.annotation.Nullable;
+
 import org.sosy_lab.solver.api.Formula;
 import org.sosy_lab.solver.api.FormulaType;
 import org.sosy_lab.solver.api.UninterpretedFunctionDeclaration;
@@ -53,7 +55,7 @@ public int hashCode() {
   }
 
   @Override
-  public boolean equals(Object obj) {
+  public boolean equals(@Nullable Object obj) {
     if (this == obj) {
       return true;
     }

diff --git a/src/org/sosy_lab/solver/basicimpl/AbstractUninterpretedFunctionDeclarationTest.java b/src/org/sosy_lab/solver/basicimpl/AbstractUninterpretedFunctionDeclarationTest.java
@@ -0,0 +1,35 @@
+/*
+ *  CPAchecker is a tool for configurable software verification.
+ *  This file is part of CPAchecker.
+ *
+ *  Copyright (C) 2007-2015  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *
+ *  CPAchecker web page:
+ *    http://cpachecker.sosy-lab.org
+ */
+package org.sosy_lab.solver.basicimpl;
+
+import org.junit.Test;
+
+public class AbstractUninterpretedFunctionDeclarationTest {
+
+  @Test
+  public void testEquals() {
+    // equals method of AbstractUninterpretedFunctionDeclaration
+    // is not testable with PackageSanityTest because of type fields
+  }
+}
diff --git a/src/org/sosy_lab/solver/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/solver/basicimpl/PackageSanityTest.java
@@ -0,0 +1,35 @@
+/*
+ *  CPAchecker is a tool for configurable software verification.
+ *  This file is part of CPAchecker.
+ *
+ *  Copyright (C) 2007-2015  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *
+ *  CPAchecker web page:
+ *    http://cpachecker.sosy-lab.org
+ */
+package org.sosy_lab.solver.basicimpl;
+
+import org.sosy_lab.solver.api.FormulaType;
+
+import com.google.common.testing.AbstractPackageSanityTests;
+
+public class PackageSanityTest extends AbstractPackageSanityTests {
+
+  {
+    setDistinctValues(FormulaType.class, FormulaType.BooleanType, FormulaType.IntegerType);
+  }
+}
diff --git a/src/org/sosy_lab/solver/logging/LoggingInterpolatingProverEnvironment.java b/src/org/sosy_lab/solver/logging/LoggingInterpolatingProverEnvironment.java
@@ -23,13 +23,15 @@
  */
 package org.sosy_lab.solver.logging;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import java.util.List;
 import java.util.Set;
 import java.util.logging.Level;
 
 import org.sosy_lab.common.log.LogManager;
-import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.Model;
+import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.api.BooleanFormula;
 import org.sosy_lab.solver.api.InterpolatingProverEnvironmentWithAssumptions;
 
@@ -41,8 +43,8 @@ public class LoggingInterpolatingProverEnvironment<T> implements InterpolatingPr
   int level = 0;
 
   public LoggingInterpolatingProverEnvironment(LogManager logger, InterpolatingProverEnvironmentWithAssumptions<T> ipe) {
-    this.wrapped = ipe;
-    this.logger = logger;
+    this.wrapped = checkNotNull(ipe);
+    this.logger = checkNotNull(logger);
   }
 
   @Override

diff --git a/src/org/sosy_lab/solver/logging/LoggingOptEnvironment.java b/src/org/sosy_lab/solver/logging/LoggingOptEnvironment.java
@@ -23,12 +23,14 @@
  */
 package org.sosy_lab.solver.logging;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import java.util.logging.Level;
 
 import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.common.rationals.Rational;
-import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.Model;
+import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.api.BooleanFormula;
 import org.sosy_lab.solver.api.Formula;
 import org.sosy_lab.solver.api.OptEnvironment;
@@ -44,8 +46,8 @@ public class LoggingOptEnvironment implements OptEnvironment {
   LogManager logger;
 
   public LoggingOptEnvironment(LogManager logger, OptEnvironment oe) {
-    this.wrapped = oe;
-    this.logger = logger;
+    this.wrapped = checkNotNull(oe);
+    this.logger = checkNotNull(logger);
   }
 
   @Override

diff --git a/src/org/sosy_lab/solver/logging/LoggingProverEnvironment.java b/src/org/sosy_lab/solver/logging/LoggingProverEnvironment.java
@@ -23,12 +23,14 @@
  */
 package org.sosy_lab.solver.logging;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import java.util.List;
 import java.util.logging.Level;
 
 import org.sosy_lab.common.log.LogManager;
-import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.Model;
+import org.sosy_lab.solver.SolverException;
 import org.sosy_lab.solver.api.BooleanFormula;
 import org.sosy_lab.solver.api.Formula;
 import org.sosy_lab.solver.api.ProverEnvironment;
@@ -43,8 +45,8 @@ public class LoggingProverEnvironment implements ProverEnvironment {
   int level = 0;
 
   public LoggingProverEnvironment(LogManager logger, ProverEnvironment pe) {
-    this.wrapped = pe;
-    this.logger = logger;
+    this.wrapped = checkNotNull(pe);
+    this.logger = checkNotNull(logger);
   }
 
   @Override

diff --git a/src/org/sosy_lab/solver/logging/PackageSanityTest.java b/src/org/sosy_lab/solver/logging/PackageSanityTest.java
@@ -0,0 +1,30 @@
+/*
+ *  CPAchecker is a tool for configurable software verification.
+ *  This file is part of CPAchecker.
+ *
+ *  Copyright (C) 2007-2015  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *
+ *  CPAchecker web page:
+ *    http://cpachecker.sosy-lab.org
+ */
+package org.sosy_lab.solver.logging;
+
+import com.google.common.testing.AbstractPackageSanityTests;
+
+public class PackageSanityTest extends AbstractPackageSanityTests {
+
+}