| import java.util.List; |
| import org.checkerframework.dataflow.qual.Pure; |
| import org.checkerframework.framework.test.*; |
| import org.checkerframework.framework.testchecker.util.*; |
| |
| public class Basic2 { |
| |
| // basic tests to make sure everything works |
| void t1(@Odd String p1, String p2) { |
| String l1 = p1; |
| // :: error: (assignment) |
| @Odd String l2 = p2; |
| } |
| |
| // basic local variable flow sensitivity |
| void t2(@Odd String p1, String p2, boolean b1) { |
| String l1 = p1; |
| if (b1) { |
| l1 = p2; |
| } |
| // :: error: (assignment) |
| @Odd String l3 = l1; |
| |
| l1 = p1; |
| while (b1) { |
| l1 = p2; |
| } |
| // :: error: (assignment) |
| @Odd String l4 = l1; |
| } |
| |
| void t2b(@Odd String p1, String p2, @Odd String p3, boolean b1) { |
| String l1 = p1; |
| |
| if (b1) { |
| l1 = p3; |
| } |
| @Odd String l3 = l1; |
| |
| while (b1) { |
| l1 = p3; |
| } |
| @Odd String l4 = l1; |
| } |
| |
| // return statement |
| void t3(@Odd String p1, String p2, boolean b1) { |
| String l1 = p1; |
| if (b1) { |
| l1 = p2; |
| return; |
| } |
| @Odd String l3 = l1; |
| } |
| |
| // simple throw statement |
| void t4(@Odd String p1, String p2, boolean b1) { |
| String l1 = p1; |
| if (b1) { |
| l1 = p2; |
| throw new RuntimeException(); |
| } |
| @Odd String l3 = l1; |
| } |
| |
| class C { |
| C c; |
| String f1, f2, f3; |
| @Odd String g1, g2, g3; |
| } |
| |
| // fields |
| void t5(@Odd String p1, String p2, boolean b1, C c1, C c2) { |
| c1.f1 = p1; |
| @Odd String l1 = c1.f1; |
| c2.f2 = p2; // assignment to f2 does not change knowledge about f1 |
| c1.f2 = p2; |
| @Odd String l2 = c1.f1; |
| c2.f1 = p2; |
| // :: error: (assignment) |
| @Odd String l3 = c1.f1; |
| } |
| |
| // fields |
| void t6(@Odd String p1, String p2, boolean b1, C c1, C c2) { |
| c1.f1 = p1; |
| c1.c.f1 = p1; |
| @Odd String l2 = c1.c.f1; |
| c1.f1 = p2; |
| // :: error: (assignment) |
| @Odd String l3 = c1.f1; |
| |
| c1.f1 = p1; |
| c1.c.f1 = p1; |
| @Odd String l4 = c1.c.f1; |
| c2.c = c2; |
| // :: error: (assignment) |
| @Odd String l5 = c1.f1; |
| // :: error: (assignment) |
| @Odd String l6 = c1.c.f1; |
| } |
| |
| // fields |
| void t6b(@Odd String p1, String p2, boolean b1, C c1, C c2) { |
| if (b1) { |
| c1.f1 = p1; |
| } |
| // :: error: (assignment) |
| @Odd String l1 = c1.f1; |
| |
| if (b1) { |
| c1.f1 = p1; |
| } else { |
| c1.f1 = p1; |
| } |
| @Odd String l2 = c1.f1; |
| } |
| |
| // method calls |
| void nonpure() {} |
| |
| @Pure |
| int pure() { |
| return 1; |
| } |
| |
| void t7(@Odd String p1, String p2, boolean b1, C c1, C c2) { |
| c1.f1 = p1; |
| nonpure(); |
| // :: error: (assignment) |
| @Odd String l1 = c1.f1; |
| |
| c1.f1 = p1; |
| pure(); |
| @Odd String l2 = c1.f1; |
| } |
| |
| // array accesses |
| void t8(@Odd String a1[], String a2[], String p3) { |
| String l1 = a1[0]; |
| |
| // :: error: (assignment) |
| @Odd String l2 = a2[0]; |
| |
| @Odd String l3 = l1; |
| |
| a1[0] = l1; |
| a1[1] = l3; |
| |
| // :: error: (assignment) |
| a1[2] = p3; |
| |
| a2[0] = l1; |
| a2[1] = l3; |
| a2[2] = p3; |
| } |
| |
| // self type |
| void t9(@Odd Basic2 this) { |
| @Odd Basic2 l1 = this; |
| } |
| |
| // generics |
| public <T extends String> void t10a(T p1, @Odd T p2) { |
| T l1 = p1; |
| p1 = l1; |
| T l2 = p2; |
| p2 = l2; |
| // :: error: (assignment) |
| @Odd T l3 = p1; |
| @Odd T l4 = p2; |
| } |
| |
| public <T extends @Odd String> void t10b(T p1, @Odd T p2) { |
| T l1 = p1; |
| p1 = l1; |
| T l2 = p2; |
| p2 = l2; |
| @Odd T l3 = p1; |
| @Odd T l4 = p2; |
| } |
| |
| // for-each loop |
| void t11(@Odd String p1, String p2, List<String> list, List<@Odd String> oddList) { |
| // :: error: (enhancedfor) |
| for (@Odd String i : list) {} |
| for (@Odd String i : oddList) { |
| @Odd String l1 = i; |
| } |
| for (@Odd String i : oddList) { |
| // :: error: (assignment) |
| i = p2; |
| } |
| for (String i : oddList) { |
| // @Odd String l3 = i; |
| } |
| } |
| |
| // cast without annotations |
| void t12(@Odd String p1, String p2, boolean b1) { |
| @Odd String l1 = (String) p1; |
| } |
| |
| // final fields |
| class CF { |
| final String f1; |
| CF c; |
| |
| void nonpure() {} |
| |
| CF(@Odd String p1) { |
| f1 = p1; |
| nonpure(); |
| @Odd String l1 = f1; |
| } |
| |
| void CF_t1(@Odd String p1, CF o) { |
| if (f1 == p1) { |
| nonpure(); |
| @Odd String l1 = f1; |
| } |
| } |
| } |
| |
| // final fields with initializer |
| class A { |
| final @Odd String f1 = null; |
| final String f2 = f1; |
| |
| void A_t1() { |
| @Odd String l1 = f2; |
| } |
| } |
| } |