File: RefineNeq.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 22,840 kB
  • sloc: java: 145,910; xml: 839; sh: 518; makefile: 401; perl: 26
file content (41 lines) | stat: -rw-r--r-- 1,208 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;

class RefineNeq {
    int[] arr = {1};

    void testLTL(@LTLengthOf("arr") int test) {
        // :: error: (assignment.type.incompatible)
        @LTLengthOf("arr") int a = Integer.parseInt("1");

        int b = 1;
        if (test != b) {
            // :: error: (assignment.type.incompatible)
            @LTLengthOf("arr") int e = b;

        } else {

            @LTLengthOf("arr") int c = b;
        }
        // :: error: (assignment.type.incompatible)
        @LTLengthOf("arr") int d = b;
    }

    void testLTEL(@LTEqLengthOf("arr") int test) {
        // :: error: (assignment.type.incompatible)
        @LTEqLengthOf("arr") int a = Integer.parseInt("1");

        int b = 1;
        if (test != b) {
            // :: error: (assignment.type.incompatible)
            @LTEqLengthOf("arr") int e = b;
        } else {
            @LTEqLengthOf("arr") int c = b;

            // :: error: (assignment.type.incompatible)
            @LTLengthOf("arr") int g = b;
        }
        // :: error: (assignment.type.incompatible)
        @LTEqLengthOf("arr") int d = b;
    }
}