aboutsummaryrefslogtreecommitdiff
path: root/compiler/tests/verifier/expr_quals.good
blob: fc315b30df56eb02ef06a7317e66d6c2f719db94 (plain)
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99


// P = pointer

// x = normal
// v = var
// s = shared
// o = owned
// g = garbage collected


// values
int x;
var int v;
shared int s;
var shared int vs;


// pointers to values
int^ xPx = @x;
shared int^ xPs = @s;
var shared int^ xPvs = @vs;

// pointers with var qualifier
int var^ vPx = @x;
shared int var^ vPs = @s;
var int var^ vPv = @v;
var int shared^ sPv = @v;
var shared int var^ vPvs = @vs;

// pointers with shared qualifier
int shared^ sPx = @x;
shared int shared^ sPs = @s;
var shared int shared^ sPvs = @vs;

// pointers with var shared qualifier
int var shared^ vsPx = @x;
shared int var shared^ vsPs = @s;
var int var shared^ vsPv = @v;
var shared int var shared^ vsPvs = @vs;


() f(var int^ xPv) {

    // Rules (T = to, F = from)
    //
    // values
    //   Town =  Fown
    //   Tgc  =  Fgc
    //   Tvar =  1    if not an initialization
    //
    // pointees, depth 1
    //   Town -> Fown
    //   Town <- Fown  if lifetime of Town is longer than Fown
    //   Tgc  =  Tgc
    //   Tvar -> Fvar
    //   Tshr <- Fshr
    //
    // pointees, deeper
    //   must be exactle the same, like in C?

    // -------------------------------------------------------------------
    // dereference and store in value
    // values are copied so this is OK
    
    // constant pointers to int
    v = xPx^;
    v = xPv^;
    v = xPs^;
    v = xPvs^;
    v = xPx^ + xPv^ + xPs^ + xPvs^;
    
    // var pointers
    v = vPx^;
    v = vPv^;
    v = vPs^;
    v = vPvs^;
    v = vPx^ + vPv^ + vPs^ + vPvs^;
    
    // shared pointers
    v = sPx^;
    v = sPv^;
    v = sPs^;
    v = sPvs^;
    v = sPx^ + sPv^ + sPs^ + sPvs^;
    
    // var shared pointers
    v = vsPx^;
    v = vsPv^;
    v = vsPs^;
    v = vsPvs^;
    v = vsPx^ + vsPv^ + vsPs^ + vsPvs^;
    
    // pointers are values
    vPx = @x;
    
    // 
}