liquidjava/liquidjava-example/src/main/java/testSuite/CorrectBareBooleanIf.java at 3ae3e9b004c0a034edbf2a80650e54af3a5d9907 · liquid-java/liquidjava · GitHub

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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
package testSuite;

import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

// Regression for issue #371: preserve both outcomes of a boolean condition.
@StateSet({"open", "closed"})
public class CorrectBareBooleanIf {
    @StateRefinement(to = "open(this)")
    public CorrectBareBooleanIf() {}
    @StateRefinement(to = "open(this)")
    public void reopen() {}
    @StateRefinement(to = "closed(this)")
    public void close() {}
    @StateRefinement(from = "open(this)")
    public void use() {}

    @Refinement("_ == value")
    public static boolean identity(boolean value) { return value; }

    public static void bothPathsSafe(boolean again) {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        if (again) {
            r.reopen();
        }
        r.use();
    }

    public static void knownTrue() {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        r.close();
        boolean again = true;
        if (again) {
            r.reopen();
        }
        r.use();
    }

    public static void knownFalseCall() {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        if (identity(false)) {
            r.close();
        }
        r.use();
    }

    public static void negatedKnownFalse() {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        r.close();
        boolean again = false;
        if (!again) {
            r.reopen();
        }
        r.use();
    }

    public static void guardedUse(boolean again) {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        r.close();
        if (again) {
            r.reopen();
        }
        if (again) {
            r.use();
        }
    }

    public static void explicitElse(boolean again) {
        CorrectBareBooleanIf r = new CorrectBareBooleanIf();
        r.close();
        if (again) {
            r.reopen();
        } else {
            r.reopen();
        }
        r.use();
    }
}