File: EnsuresNonNullIfTest4.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (31 lines) | stat: -rw-r--r-- 790 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
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.*;

public class EnsuresNonNullIfTest4 {

    public void add_bottom_up(MyInvariant inv) {

        // The problem goes away if the below line is deleted or replaced with:
        //   Object x = new Object[100];
        Object x = new @Nullable Object[100];

        if (inv.is_ni_suppressed()) {
            Object ss = inv.get_ni_suppressions();
            ss.toString();
        }
    }
}

class MyInvariant {
    @Pure
    public @Nullable Object get_ni_suppressions() {
        return (null);
    }

    @SuppressWarnings("nullness")
    @EnsuresNonNullIf(result = true, expression = "get_ni_suppressions()")
    @Pure
    public boolean is_ni_suppressed() {
        return true;
    }
}