Bael 1490 the checker framework and java pluggable type systems (#3584)
* BAEL-1490 First examples, Maven setup * BAEL-1490 Each checker has its own source file * BAEL-1490 Added checker for String.format * BAEL-1490 The Checker Framework and Java Pluggable Type Systems * Added comments, removed example that is probably too technical for a brad audience.
This commit is contained in:
parent
a72246af2f
commit
b35b913cbe
|
@ -0,0 +1,114 @@
|
||||||
|
<project xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://maven.apache.org/POM/4.0.0"
|
||||||
|
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">
|
||||||
|
<modelVersion>4.0.0</modelVersion>
|
||||||
|
<groupId>com.baeldung</groupId>
|
||||||
|
<artifactId>checker-plugin</artifactId>
|
||||||
|
<packaging>jar</packaging>
|
||||||
|
<version>1.0-SNAPSHOT</version>
|
||||||
|
<name>checker-plugin</name>
|
||||||
|
<url>http://maven.apache.org</url>
|
||||||
|
|
||||||
|
<!-- https://checkerframework.org/manual/#maven -->
|
||||||
|
|
||||||
|
<properties>
|
||||||
|
<!-- These properties will be set by the Maven Dependency plugin -->
|
||||||
|
<annotatedJdk>${org.checkerframework:jdk8:jar}</annotatedJdk>
|
||||||
|
<!-- Uncomment to use the Type Annotations compiler. -->
|
||||||
|
<!--
|
||||||
|
<typeAnnotationsJavac>${org.checkerframework:compiler:jar}</typeAnnotationsJavac>
|
||||||
|
-->
|
||||||
|
</properties>
|
||||||
|
|
||||||
|
<dependencies>
|
||||||
|
|
||||||
|
|
||||||
|
<!-- Annotations from the Checker Framework: nullness, interning, locking, ... -->
|
||||||
|
<dependency>
|
||||||
|
<groupId>org.checkerframework</groupId>
|
||||||
|
<artifactId>checker-qual</artifactId>
|
||||||
|
<version>2.3.1</version>
|
||||||
|
</dependency>
|
||||||
|
<dependency>
|
||||||
|
<groupId>org.checkerframework</groupId>
|
||||||
|
<artifactId>checker</artifactId>
|
||||||
|
<version>2.3.1</version>
|
||||||
|
</dependency>
|
||||||
|
<dependency>
|
||||||
|
<groupId>org.checkerframework</groupId>
|
||||||
|
<artifactId>jdk8</artifactId>
|
||||||
|
<version>2.3.1</version>
|
||||||
|
</dependency>
|
||||||
|
<!-- The Type Annotations compiler. Uncomment if using annotations in comments. -->
|
||||||
|
<dependency>
|
||||||
|
<groupId>org.checkerframework</groupId>
|
||||||
|
<artifactId>compiler</artifactId>
|
||||||
|
<version>2.3.1</version>
|
||||||
|
</dependency>
|
||||||
|
|
||||||
|
</dependencies>
|
||||||
|
|
||||||
|
<build>
|
||||||
|
<plugins>
|
||||||
|
|
||||||
|
<plugin>
|
||||||
|
<!-- This plugin will set properties values using dependency information -->
|
||||||
|
<groupId>org.apache.maven.plugins</groupId>
|
||||||
|
<artifactId>maven-dependency-plugin</artifactId>
|
||||||
|
<executions>
|
||||||
|
<execution>
|
||||||
|
<goals>
|
||||||
|
<!--
|
||||||
|
Goal that sets a property pointing to the artifact file for each project dependency.
|
||||||
|
For each dependency (direct and transitive) a project property will be set which
|
||||||
|
follows the:
|
||||||
|
|
||||||
|
groupId:artifactId:type:[classifier]
|
||||||
|
|
||||||
|
form and contains the path to the resolved artifact. -->
|
||||||
|
<goal>properties</goal>
|
||||||
|
</goals>
|
||||||
|
</execution>
|
||||||
|
</executions>
|
||||||
|
</plugin>
|
||||||
|
|
||||||
|
<plugin>
|
||||||
|
<artifactId>maven-compiler-plugin</artifactId>
|
||||||
|
<version>3.6.1</version>
|
||||||
|
<configuration>
|
||||||
|
<source>1.8</source>
|
||||||
|
<target>1.8</target>
|
||||||
|
<!-- Uncomment the following line to use the type annotations compiler. -->
|
||||||
|
<!-- <fork>true</fork> -->
|
||||||
|
<compilerArguments>
|
||||||
|
<Xmaxerrs>10000</Xmaxerrs>
|
||||||
|
<Xmaxwarns>10000</Xmaxwarns>
|
||||||
|
</compilerArguments>
|
||||||
|
<annotationProcessors>
|
||||||
|
<!-- Add all the checkers you want to enable here -->
|
||||||
|
<annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
|
||||||
|
<annotationProcessor>org.checkerframework.checker.interning.InterningChecker</annotationProcessor>
|
||||||
|
<annotationProcessor>org.checkerframework.checker.fenum.FenumChecker</annotationProcessor>
|
||||||
|
<annotationProcessor>org.checkerframework.checker.formatter.FormatterChecker</annotationProcessor>
|
||||||
|
<annotationProcessor>org.checkerframework.checker.regex.RegexChecker</annotationProcessor>
|
||||||
|
</annotationProcessors>
|
||||||
|
<compilerArgs>
|
||||||
|
<arg>-AprintErrorStack</arg>
|
||||||
|
|
||||||
|
<!-- location of the annotated JDK, which comes from a Maven dependency -->
|
||||||
|
<arg>-Xbootclasspath/p:${annotatedJdk}</arg>
|
||||||
|
<!--
|
||||||
|
-->
|
||||||
|
|
||||||
|
<!-- Uncomment the following line to use the type annotations compiler. -->
|
||||||
|
<!--
|
||||||
|
<arg>-J-Xbootclasspath/p:${typeAnnotationsJavac}</arg>
|
||||||
|
-->
|
||||||
|
<!-- Uncomment the following line to turn type-checking warnings into errors. -->
|
||||||
|
<arg>-Awarns</arg>
|
||||||
|
</compilerArgs>
|
||||||
|
</configuration>
|
||||||
|
</plugin>
|
||||||
|
</plugins>
|
||||||
|
</build>
|
||||||
|
|
||||||
|
</project>
|
|
@ -0,0 +1,42 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
import org.checkerframework.checker.fenum.qual.Fenum;
|
||||||
|
|
||||||
|
//@SuppressWarnings("fenum:assignment.type.incompatible")
|
||||||
|
public class FakeNumExample {
|
||||||
|
|
||||||
|
// Here we use some String constants to represents countries.
|
||||||
|
static final @Fenum("country") String ITALY = "IT";
|
||||||
|
static final @Fenum("country") String US = "US";
|
||||||
|
static final @Fenum("country") String UNITED_KINGDOM = "UK";
|
||||||
|
|
||||||
|
// Here we use other String constants to represent planets instead.
|
||||||
|
static final @Fenum("planet") String MARS = "Mars";
|
||||||
|
static final @Fenum("planet") String EARTH = "Earth";
|
||||||
|
static final @Fenum("planet") String VENUS = "Venus";
|
||||||
|
|
||||||
|
// Now we write this method and we want to be sure that
|
||||||
|
// the String parameter has a value of a country, not that is just a String.
|
||||||
|
void greetCountries(@Fenum("country") String country) {
|
||||||
|
System.out.println("Hello " + country);
|
||||||
|
}
|
||||||
|
|
||||||
|
// Similarly we're enforcing here that the provided
|
||||||
|
// parameter is a String that represent a planet.
|
||||||
|
void greetPlanets(@Fenum("planet") String planet) {
|
||||||
|
System.out.println("Hello " + planet);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static void main(String[] args) {
|
||||||
|
|
||||||
|
FakeNumExample obj = new FakeNumExample();
|
||||||
|
|
||||||
|
// This will fail because we pass a planet-String to a method that
|
||||||
|
// accept a country-String.
|
||||||
|
obj.greetCountries(MARS);
|
||||||
|
|
||||||
|
// Here the opposite happens.
|
||||||
|
obj.greetPlanets(US);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,23 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
public class FormatExample {
|
||||||
|
|
||||||
|
public static void main(String[] args) {
|
||||||
|
|
||||||
|
// Just enabling org.checkerframework.checker.formatter.FormatterChecker
|
||||||
|
// we can be sure at compile time that the format strings we pass to format()
|
||||||
|
// are correct. Normally we would have those errors raised just at runtime.
|
||||||
|
// All those formats are in fact wrong.
|
||||||
|
|
||||||
|
String.format("%y", 7); // error: invalid format string
|
||||||
|
|
||||||
|
String.format("%d", "a string"); // error: invalid argument type for %d
|
||||||
|
|
||||||
|
String.format("%d %s", 7); // error: missing argument for %s
|
||||||
|
|
||||||
|
String.format("%d", 7, 3); // warning: unused argument 3
|
||||||
|
|
||||||
|
String.format("{0}", 7); // warning: unused argument 7, because {0} is wrong syntax
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,31 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
import org.checkerframework.checker.nullness.qual.KeyFor;
|
||||||
|
|
||||||
|
import java.util.HashMap;
|
||||||
|
import java.util.Map;
|
||||||
|
|
||||||
|
public class KeyForExample {
|
||||||
|
|
||||||
|
private final Map<String, String> config = new HashMap<>();
|
||||||
|
|
||||||
|
KeyForExample() {
|
||||||
|
|
||||||
|
// Here we initialize a map to store
|
||||||
|
// some config data.
|
||||||
|
config.put("url", "http://1.2.3.4");
|
||||||
|
config.put("name", "foobaz");
|
||||||
|
}
|
||||||
|
|
||||||
|
public void dumpPort() {
|
||||||
|
|
||||||
|
// Here, we want to dump the port value stored in the
|
||||||
|
// config, so we declare that this key has to be
|
||||||
|
// present in the config map.
|
||||||
|
// Obviously that will fail because such key is not present
|
||||||
|
// in the map.
|
||||||
|
@KeyFor("config") String key = "port";
|
||||||
|
System.out.println( config.get(key) );
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,28 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
|
||||||
|
|
||||||
|
import java.util.Date;
|
||||||
|
|
||||||
|
public class MonotonicNotNullExample {
|
||||||
|
|
||||||
|
// The idea is we need this field to be to lazily initialized,
|
||||||
|
// so it starts as null but once it becomes not null
|
||||||
|
// it cannot return null.
|
||||||
|
// In these cases, we can use @MonotonicNonNull
|
||||||
|
@MonotonicNonNull private Date firstCall;
|
||||||
|
|
||||||
|
public Date getFirstCall() {
|
||||||
|
if (firstCall == null) {
|
||||||
|
firstCall = new Date();
|
||||||
|
}
|
||||||
|
return firstCall;
|
||||||
|
}
|
||||||
|
|
||||||
|
public void reset() {
|
||||||
|
// This is reported as error because
|
||||||
|
// we wrongly set the field back to null.
|
||||||
|
firstCall = null;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,27 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
import org.checkerframework.checker.nullness.qual.NonNull;
|
||||||
|
import org.checkerframework.checker.nullness.qual.Nullable;
|
||||||
|
|
||||||
|
public class NonNullExample {
|
||||||
|
|
||||||
|
// This method's parameter is annotated in order
|
||||||
|
// to tell the pluggable type system that it can never be null.
|
||||||
|
private static int countArgs(@NonNull String[] args) {
|
||||||
|
return args.length;
|
||||||
|
}
|
||||||
|
|
||||||
|
// This method's parameter is annotated in order
|
||||||
|
// to tell the pluggable type system that it may be null.
|
||||||
|
public static void main(@Nullable String[] args) {
|
||||||
|
|
||||||
|
// Here lies a potential error,
|
||||||
|
// because we pass a potential null reference to a method
|
||||||
|
// that does not accept nulls.
|
||||||
|
// The Checker Framework will spot this problem at compile time
|
||||||
|
// instead of runtime.
|
||||||
|
System.out.println(countArgs(args));
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,18 @@
|
||||||
|
package com.baeldung.typechecker;
|
||||||
|
|
||||||
|
import org.checkerframework.checker.regex.qual.Regex;
|
||||||
|
|
||||||
|
public class RegexExample {
|
||||||
|
|
||||||
|
// For some reason we want to be sure that this regex
|
||||||
|
// contains at least one capturing group.
|
||||||
|
// However, we do an error and we forgot to define such
|
||||||
|
// capturing group in it.
|
||||||
|
@Regex(1) private static String findNumbers = "\\d*";
|
||||||
|
|
||||||
|
public static void main(String[] args) {
|
||||||
|
String message = "My phone number is +3911223344.";
|
||||||
|
message.matches(findNumbers);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
Loading…
Reference in New Issue