checker/tests/tainting/Buffer.java

import java.util.ArrayList;
import java.util.List;
import org.checkerframework.checker.tainting.qual.PolyTainted;
import org.checkerframework.checker.tainting.qual.Tainted;
import org.checkerframework.checker.tainting.qual.Untainted;
import org.checkerframework.framework.qual.HasQualifierParameter;

@HasQualifierParameter(Tainted.class)
public class Buffer {
  final List<@PolyTainted String> list = new ArrayList<>();
  @PolyTainted String someString = "";
  // :: error: (invalid.polymorphic.qualifier.use)
  static @PolyTainted Object staticField;

  public @PolyTainted Buffer() {}

  public @Untainted Buffer(@Tainted String s) {
    // :: error: (assignment)
    this.someString = s;
  }

  public @PolyTainted Buffer(@PolyTainted Buffer copy) {}

  public @PolyTainted Buffer append(@PolyTainted Buffer this, @PolyTainted String s) {
    list.add(s);
    someString = s;
    return this;
  }

  public @PolyTainted String prettyPrint(@PolyTainted Buffer this) {
    String prettyString = "";
    for (String s : list) {
      prettyString += s + " ~~ ";
    }
    return prettyString;
  }

  public @PolyTainted String unTaintedOnly(@Untainted Buffer this, @PolyTainted String s) {
    // :: error: (argument)
    list.add(s);
    // :: error: (assignment)
    someString = s;
    return s;
  }

  static class Use {
    void passingUses(@Untainted String untainted, @Untainted Buffer buffer) {
      buffer.list.add(untainted);
      buffer.someString = untainted;
      buffer.append(untainted);
    }

    void failingUses(@Tainted String tainted, @Untainted Buffer buffer) {
      // :: error: (argument)
      buffer.list.add(tainted);
      // :: error: (assignment)
      buffer.someString = tainted;
      // :: error: (argument)
      buffer.append(tainted);
    }

    void casts(@Untainted Object untainted, @Tainted Object tainted) {
      @Untainted Buffer b1 = (@Untainted Buffer) untainted; // ok
      // :: error: (invariant.cast.unsafe)
      @Untainted Buffer b2 = (@Untainted Buffer) tainted;

      // :: error: (invariant.cast.unsafe)
      @Tainted Buffer b3 = (@Tainted Buffer) untainted; // error
      // :: error: (invariant.cast.unsafe)
      @Tainted Buffer b4 = (@Tainted Buffer) tainted; // error

      @Untainted Buffer b5 = (Buffer) untainted; // ok
      // :: error: (invariant.cast.unsafe)
      @Tainted Buffer b6 = (Buffer) tainted;
    }

    void creation() {
      @Untainted Buffer b1 = new @Untainted Buffer();
      @Tainted Buffer b2 = new @Tainted Buffer();
      @PolyTainted Buffer b3 = new @PolyTainted Buffer();
    }
  }
}