checker/tests/tainting/Casts.java

import org.checkerframework.checker.tainting.qual.Tainted;
import org.checkerframework.checker.tainting.qual.Untainted;
import org.checkerframework.framework.qual.HasQualifierParameter;

public class Casts {
  @HasQualifierParameter(Tainted.class)
  static class Buffer {}

  @HasQualifierParameter(Tainted.class)
  static class MyBuffer extends Buffer {}

  void test(
      @Tainted Buffer taintedBuf,
      @Untainted Buffer untaintedBuf,
      @Tainted Object taintedObj,
      @Untainted Object untaintedObj) {
    @Tainted Object o = (@Tainted Object) taintedBuf;
    o = (@Tainted Object) untaintedObj;
    o = (@Tainted Object) untaintedBuf;

    // :: error: (invariant.cast.unsafe)
    o = (@Tainted Buffer) taintedObj;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted Buffer) untaintedBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted Buffer) untaintedObj;

    // :: warning: (cast.unsafe)
    o = (@Untainted Object) taintedObj;
    // :: warning: (cast.unsafe)
    o = (@Untainted Object) taintedBuf;
    o = (@Untainted Object) untaintedBuf;

    // :: error: (invariant.cast.unsafe)
    o = (@Untainted Buffer) taintedObj;
    // :: error: (invariant.cast.unsafe)
    o = (@Untainted Buffer) taintedBuf;
    o = (@Untainted Buffer) untaintedObj;
  }

  void test2(
      @Tainted Buffer taintedBuf,
      @Untainted Buffer untaintedBuf,
      @Tainted MyBuffer taintedMyBuf,
      @Untainted MyBuffer untaintedMyBuff) {
    @Tainted Object o = (@Tainted Buffer) taintedMyBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted Buffer) untaintedBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted Buffer) untaintedMyBuff;

    o = (@Tainted MyBuffer) taintedBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted MyBuffer) untaintedBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Tainted MyBuffer) untaintedMyBuff;

    // :: error: (invariant.cast.unsafe)
    o = (@Untainted Buffer) taintedMyBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Untainted Buffer) taintedMyBuf;
    o = (@Untainted Buffer) untaintedMyBuff;

    // :: error: (invariant.cast.unsafe)
    o = (@Untainted MyBuffer) taintedBuf;
    // :: error: (invariant.cast.unsafe)
    o = (@Untainted MyBuffer) taintedMyBuf;
    o = (@Untainted MyBuffer) untaintedMyBuff;
  }
}