Replace FindBugs with its successor SpotBugs.

The first release of SpotBugs is backwards compatible, so almost nothing
changes, but you need to run "ant spotbugs" now.

Furthermore, we need to add a dependency on jsr305 for the
javax.annotations package, which was previously included in the
findbugs-annotations package, but this was actually bad because Guava
also has a dependency on jsr305, so we ended up with the annotations
twice on the class path.
In the future, we will probably need to migrate away from these
annotations, as both SpotBugs and Guava consider:
spotbugs/spotbugs#130
spotbugs/spotbugs#180
google/guava#2960

.classpath

@@ -14,7 +14,8 @@
 	<classpathentry kind="lib" path="lib/java/build/auto-value.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/truth-java8-extension.jar" sourcepath="lib/java-contrib/truth-java8-extension-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/byte-buddy.jar"/>
-	<classpathentry kind="lib" path="lib/java/runtime/annotations.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime/spotbugs-annotations.jar" sourcepath="lib/java-contrib/spotbugs-annotations-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime/jsr305.jar" sourcepath="lib/java-contrib/jsr305-sources.jar"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
 	<classpathentry kind="src" path=".apt-generated">
 		<attributes>

.settings/FindBugs.exclude.xml → .settings/SpotBugs.exclude.xml

@@ -1,11 +1,11 @@
 <FindBugsFilter>
     <Match><And>
         <!-- PackageSanityTest wants @Nullable on equals(Object) parameter,
-             FindBugs does not. -->
+             SpotBugs does not. -->
         <Bug pattern="NP_METHOD_PARAMETER_TIGHTENS_ANNOTATION"/>
         <Method name="equals" returns="boolean" params="java.lang.Object"/>
     </And></Match>
-    <!-- Error-prone checks this, too, and FindBugs does not know @CanIgnoreReturnValue. -->
+    <!-- Error-prone checks this, too, and SpotBugs does not know @CanIgnoreReturnValue. -->
     <Match><Bug pattern="RV_RETURN_VALUE_IGNORED"/></Match>
     <!-- Exclude AutoValue classes -->
     <Match><Class name="~.*\.AutoValue_.*"/></Match>

.travis.yml

@@ -25,9 +25,9 @@ matrix:
     - env: NAME=Checkstyle
       script:
         - ant run-checkstyle -Dcheckstyle.output=plain && cat Checkstyle*.xml && [ $(cat Checkstyle*.xml | grep -vic audit) -eq 0 ]
-    - env: NAME=FindBugs
+    - env: NAME=SpotBugs
       script:
-        - ant run-findbugs -Dfindbugs.output=text && cat FindBugs.xml && test \! -s FindBugs.xml
+        - ant run-spotbugs -Dspotbugs.output=text && cat SpotBugs.xml && test \! -s SpotBugs.xml
     - env: NAME='Check source-code format'
       script:
         - ant format-source && git diff -s --exit-code

build.xml

@@ -7,7 +7,7 @@
     <property file="build.properties"/>
     <property environment="env"/>
 
-    <property name="ivy.configurations" value="build, runtime, test, format-source, checkstyle, findbugs"/>
+    <property name="ivy.configurations" value="build, runtime, test, format-source, checkstyle, spotbugs"/>
     <property name="package" value="common"/>
 
     <!-- Maven Central metadata -->
@@ -25,7 +25,7 @@
     <import file="build/build-junit.xml"/>
     <import file="build/build-format-source.xml"/>
     <import file="build/build-checkstyle.xml"/>
-    <import file="build/build-findbugs.xml"/>
+    <import file="build/build-spotbugs.xml"/>
     <import file="build/build-publish.xml"/>
     <import file="build/build-maven-publish.xml"/>
 
@@ -78,5 +78,5 @@
 
     <target name="build-dependencies" depends="init, resolve-dependencies"/>
 
-    <target name="standard-checks" depends="tests, findbugs, checkstyle, javadoc"/>
+    <target name="standard-checks" depends="tests, spotbugs, checkstyle, javadoc"/>
 </project>

build/build-ivy.xml

@@ -12,7 +12,7 @@
     <!-- <property name="ivy.disable" value=""/> --> <!-- Disable ivy completely. -->
     <property name="ivy.repo.url" value="https://www.sosy-lab.org/ivy"/>
     <property name="ivy.lib.dir" value="lib/java"/>
-    <property name="ivy.configurations" value="build, runtime, test, findbugs"/>
+    <property name="ivy.configurations" value="build, runtime, test, spotbugs"/>
     <property name="ivy.settings.file" value="ivysettings.xml"/>
 
     <property name="ivy.jar.dir" value="${ivy.lib.dir}/build"/>

build/build-spotbugs.xml

@@ -0,0 +1,64 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="spotbugs" basedir=".">
+
+    <!-- Targets for running SpotBugs. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker, JavaSMT, and VerifierCloud. -->
+    <property name="spotbugs.output" value="xml:withMessages"/>
+
+    <path id="spotbugs.classpath">
+        <fileset dir="${ivy.lib.dir}/spotbugs" includes="*.jar"/>
+    </path>
+
+    <target name="run-spotbugs" depends="jar">
+        <delete file="SpotBugs.html"/>
+        <taskdef resource="edu/umd/cs/findbugs/anttask/tasks.properties" classpathref="spotbugs.classpath"/>
+        <spotbugs
+                output="${spotbugs.output}"
+                outputFile="SpotBugs.xml"
+                excludeFilter=".settings/SpotBugs.exclude.xml"
+                warningsProperty="spotbugs.warnings">
+            <auxClasspath refid="classpath" />
+            <sourcePath path="${source.dir}" />
+            <class location="${jar.file}" />
+            <classpath refid="spotbugs.classpath" />
+        </spotbugs>
+    </target>
+
+    <target name="spotbugs-report" if="spotbugs.warnings">
+        <echo>SpotBugs found warnings, generating report.</echo>
+        <xslt in="SpotBugs.xml" out="SpotBugs.html">
+            <style><javaresource classpathref="spotbugs.classpath" name="fancy.xsl"/></style>
+        </xslt>
+    </target>
+
+    <target name="spotbugs" depends="run-spotbugs, spotbugs-report" description="Run SpotBugs and generate report."/>
+
+    <target name="run-spotbugs-diff" depends="jar">
+        <delete file="SpotBugs.diff.html"/>
+        <taskdef resource="edu/umd/cs/findbugs/anttask/tasks.properties" classpathref="spotbugs.classpath"/>
+        <spotbugs
+                output="${spotbugs.output}"
+                outputFile="SpotBugs.diff.xml"
+                excludeFilter=".settings/SpotBugs.exclude.xml"
+                warningsProperty="spotbugs.newwarnings"
+                baselineBugs="SpotBugs.known.xml">
+            <auxClasspath refid="classpath" />
+            <sourcePath path="${source.dir}" />
+            <class location="${jar.file}" />
+            <classpath refid="spotbugs.classpath" />
+        </spotbugs>
+    </target>
+
+    <target name="spotbugs-diff-report" if="spotbugs.newwarnings">
+        <echo>SpotBugs found new warnings, generating report.</echo>
+        <xslt in="SpotBugs.diff.xml" out="SpotBugs.diff.html">
+            <style><javaresource classpathref="spotbugs.classpath" name="fancy.xsl"/></style>
+        </xslt>
+    </target>
+
+    <target name="spotbugs-diff" depends="run-spotbugs-diff, spotbugs-diff-report" description="Run SpotBugs and generate report with newly found warnings."/>
+
+    <target name="spotbugs-full" depends="spotbugs, spotbugs-diff" description="Run SpotBugs and generate full report and report with newly found warnings."/>
+</project>

ivy.xml

@@ -19,7 +19,7 @@
 
         <conf name="checkstyle" visibility="private" description="for running CheckStyle"/>
 
-        <conf name="findbugs" visibility="private" description="for running FindBugs"/>
+        <conf name="spotbugs" visibility="private" description="for running SpotBugs"/>
 
         <!-- Additional files like JavaDocs or source code that will help developers.
              These are not downloaded by default, but only when "ant install-contrib" is called. -->
@@ -91,10 +91,11 @@
         <!-- Checkstyle -->
         <dependency org="com.github.sevntu-checkstyle" name="sevntu-checks" rev="1.24.2" conf="checkstyle->default"/>
 
-        <!-- FindBugs -->
-        <dependency org="com.google.code.findbugs" name="findbugs" rev="3.0.1" conf="findbugs->default"/>
+        <!-- SpotBugs -->
+        <dependency org="com.github.spotbugs" name="spotbugs-ant" rev="3.1.0" conf="spotbugs->default"/>
         <!-- JAR with annotations needs to be present at runtime because we use Nullable.class -->
-        <dependency org="com.google.code.findbugs" name="annotations" rev="3.0.0" conf="runtime->default"/>
+        <dependency org="com.github.spotbugs" name="spotbugs-annotations" rev="3.1.0" conf="runtime->default; contrib->sources"/>
+        <dependency org="com.google.code.findbugs" name="jsr305" rev="3.0.2" conf="runtime->default; contrib->sources"/>
 
         <!-- Guava has a dependency on error_prone_annotations without a revision number, need an override. -->
         <override org="com.google.errorprone" module="error_prone_annotations" rev="2.1.2"/>