あいぼーいの部屋

@I_BOY_1204がJavaやJavaScriptに関して調べた事を忘れない様につらつらと記述する備忘録です。

MavenでCheckerFrameworkを使う

ChecherFramwork

前の記事では、IntelliJでCheckerFrameworkを使う方法を書きましたが、本記事では、MavenでCheckerFrameworkを使って書かれたコードをコンパイルする方法を書きます。

すでに、Maven Centralに必要なjarは上がっていますので、特に難しいことはなく、pom.xmlをきちんと書いてあげればイイだけです。
前回の記事と同様、The Checker Framework Manual: Custom pluggable types for Javaにmavenでの使い方も書いてありますが、英語しかないので、ざっくり備忘録も兼ねて書いておきます。

JDK8からアノテーションの利用できる場所が変更になってこともあり、CheckFramework上でのアノテーションの書き方がJDK8とJDK7以前とでは違います。

そのため、JDK7以前のソースコードに対して、CheckerFrameworkを利用する場合は、タイプアノテーションコンパイラを利用してください。

具体的な手順は以下のとおりです。

1, 必要な依存関係を追加します 

         <!-- annotations from the Checker Framework: nullness, interning, locking, ... -->
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>checker-qual</artifactId>
            <version>2.0.0</version>
        </dependency>
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>checker</artifactId>
            <version>2.0.0</version>
        </dependency>
        <!-- タイプアノテーションコパイラを利用する場合は以下も使う -->
        <!-- <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>compiler</artifactId>
            <version>2.0.0</version>
        </dependency> -->
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>jdk8</artifactId>
            <version>2.0.0</version>
        </dependency>

2, Mavenで使うプロパティを設定します

<properties>
    <!-- These properties will be set by the Maven Dependency plugin -->
    <annotatedJdk>${org.checkerframework:jdk8:jar}</annotatedJdk>
    <!-- タイプアノテーションコンパイラを使いたい場合はこちらを使う -->
    <!-- <typeAnnotationsJavac>${org.checkerframework:compiler:jar}</typeAnnotationsJavac> -->
</properties>

ここで、${org.checkerframework:jdk8:jar}はMavenのプロパティ参照なので、${CHECKERFRAMEWORK}/checker/dist/jdk8.jarが取得できるようにプロパティを設定する必要があります。もちろん、に${CHECKERFRAMEWORK}/checker/dist/jdk8.jarを書いても動きます。
また、maven-dependency-pluginを利用できるように以下のようにpluginの設定を追加します。

    <plugin>
        <groupId>org.apache.maven.plugins</groupId>
        <artifactId>maven-dependency-plugin</artifactId>
        <version>2.3</version>
        <executions>
            <execution>
                <goals>
                    <goal>properties</goal>
                </goals>
            </execution>
        </executions>
    </plugin>

3, maven-compiler-pluginの設定を記述します

   <plugin>
        <artifactId>maven-compiler-plugin</artifactId>
        <version>3.3</version>
        <configuration>
            <source>1.8</source>
            <target>1.8</target>
            <fork>true</fork>
            <annotationProcessors>
                <!-- 使いたいチェッカーが他にもある場合は、FQクラス名を追加します-->
                <annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
            </annotationProcessors>
            <compilerArgs>
                <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
                <!-- もしTypeAnnotationsJavacの値を使いたい場合はこちらを記述-->
                <!-- <arg>-J-Xbootclasspath/p:${typeAnnotationsJavac}</arg> -->
            </compilerArgs>
        </configuration>
    </plugin>

4, mavenを実行する

上記をまとめたpom.xmlとその実行結果は以下のようになります。
[pom.xml]

<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0"
         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
    <modelVersion>4.0.0</modelVersion>

    <groupId>com.iboy</groupId>
    <artifactId>checkerSample</artifactId>
    <version>1.0-SNAPSHOT</version>

    <properties>
        <org.checkerframework>${env.CHECKERFRAMEWORK}</org.checkerframework>
        <annotatedJdk>${org.checkerframework}</annotatedJdk>
    </properties>

    <build>
        <plugins>
            <plugin>
                <groupId>org.apache.maven.plugins</groupId>
                <artifactId>maven-dependency-plugin</artifactId>
                <version>2.3</version>
                <executions>
                    <execution>
                        <goals>
                            <goal>properties</goal>
                        </goals>
                    </execution>
                </executions>
            </plugin>
            <plugin>
                <artifactId>maven-compiler-plugin</artifactId>
                <version>3.3</version>
                <configuration>
                    <source>1.8</source>
                    <target>1.8</target>
                    <encoding>utf-8</encoding>
                    <fork>true</fork>
                    <annotationProcessors>
                        <annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
                    </annotationProcessors>
                    <compilerArgs>
                        <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
                    </compilerArgs>
                </configuration>
            </plugin>
        </plugins>
    </build>
    <dependencies>
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>checker-qual</artifactId>
            <version>2.0.0</version>
        </dependency>
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>checker</artifactId>
            <version>2.0.0</version>
        </dependency>
        <dependency>
            <groupId>org.checkerframework</groupId>
            <artifactId>jdk8</artifactId>
            <version>2.0.0</version>
        </dependency>
    </dependencies>

</project>

[実行結果]
エラーがある場合は、以下のように出力されます。
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.3:compile (default-compile) on project checkerSample: Compilation failure
[ERROR] ../checkerSample/src/main/java/NullnessExample.java:[7,35] エラー: [assignment.type.incompatible] incompatible types in assignment.
[ERROR] -> [Help 1]
※Javaソースコードは前の記事と同じものを使用