SnaKt/formver.compiler-plugin/testData/diagnostics/conversion/classes/inheritance_fields.fir.diag.txt at 765becf0d57a86405d0d888ad9dd802222d96a01 · JetBrains/SnaKt · 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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
/inheritance_fields.kt:(227,234): info: Generated Viper text for createB:
field bf$fieldNotOverride: Ref

method con$c$B$T$FieldB$T$B(p$fieldOverride: Ref) returns (ret: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$fieldOverride), df$rt$c$FieldB())
  requires acc(p$c$FieldB$shared(p$fieldOverride), wildcard)
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$B())
  ensures acc(p$c$B$shared(ret), wildcard)
  ensures acc(p$c$B$unique(ret), write)


method con$c$FieldB$T$FieldB() returns (ret: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$FieldB())
  ensures acc(p$c$FieldB$shared(ret), wildcard)
  ensures acc(p$c$FieldB$unique(ret), write)


method f$createB$TF$T$Unit() returns (ret$0: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var l0$fieldB: Ref
  var l0$b: Ref
  var l0$fieldOverride: Ref
  var anon$0: Ref
  var l0$fieldNotOverride: Ref
  l0$fieldB := con$c$FieldB$T$FieldB()
  l0$b := con$c$B$T$FieldB$T$B(l0$fieldB)
  anon$0 := pg$public$fieldOverride(l0$b)
  l0$fieldOverride := anon$0
  inhale df$rt$isSubtype(df$rt$typeOf(l0$fieldOverride), df$rt$c$FieldB())
  inhale acc(p$c$FieldB$shared(l0$fieldOverride), wildcard)
  unfold acc(p$c$B$shared(l0$b), wildcard)
  unfold acc(p$c$A$shared(l0$b), wildcard)
  l0$fieldNotOverride := l0$b.bf$fieldNotOverride
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}

method pg$public$fieldOverride(this$dispatch: Ref) returns (ret: Ref)


/inheritance_fields.kt:(699,715): info: Generated Viper text for createBFsAndNoBF:
field bf$x: Ref

method con$c$FirstBackingFieldClass$T$FirstBackingFieldClass()
  returns (ret: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$FirstBackingFieldClass())
  ensures acc(p$c$FirstBackingFieldClass$shared(ret), wildcard)
  ensures acc(p$c$FirstBackingFieldClass$unique(ret), write)


method con$c$NoBackingFieldClass$T$NoBackingFieldClass() returns (ret: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$NoBackingFieldClass())
  ensures acc(p$c$NoBackingFieldClass$shared(ret), wildcard)
  ensures acc(p$c$NoBackingFieldClass$unique(ret), write)


method con$c$SecondBackingFieldClass$T$Int$T$SecondBackingFieldClass(p$x: Ref)
  returns (ret: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$SecondBackingFieldClass())
  ensures acc(p$c$SecondBackingFieldClass$shared(ret), wildcard)
  ensures acc(p$c$SecondBackingFieldClass$unique(ret), write)
  ensures df$rt$intFromRef((unfolding acc(p$c$SecondBackingFieldClass$shared(ret), wildcard) in
      ret.bf$x)) ==
    df$rt$intFromRef(p$x)


method f$createBFsAndNoBF$TF$T$Unit() returns (ret$0: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var l0$fbf: Ref
  var l0$fbfx: Ref
  var anon$0: Ref
  var l0$nbf: Ref
  var l0$nbfx: Ref
  var anon$1: Ref
  var l0$sbf: Ref
  var l0$sbfx: Ref
  l0$fbf := con$c$FirstBackingFieldClass$T$FirstBackingFieldClass()
  anon$0 := pg$public$x(l0$fbf)
  l0$fbfx := anon$0
  inhale df$rt$isSubtype(df$rt$typeOf(l0$fbfx), df$rt$intType())
  l0$nbf := con$c$NoBackingFieldClass$T$NoBackingFieldClass()
  anon$1 := pg$public$x(l0$nbf)
  l0$nbfx := anon$1
  inhale df$rt$isSubtype(df$rt$typeOf(l0$nbfx), df$rt$intType())
  l0$sbf := con$c$SecondBackingFieldClass$T$Int$T$SecondBackingFieldClass(df$rt$intToRef(10))
  unfold acc(p$c$SecondBackingFieldClass$shared(l0$sbf), wildcard)
  l0$sbfx := l0$sbf.bf$x
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}

method pg$public$x(this$dispatch: Ref) returns (ret: Ref)


/inheritance_fields.kt:(1038,1045): info: Generated Viper text for createY:
field bf$a: Ref

method con$c$Y$T$Int$T$Y(p$a: Ref) returns (ret: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$a), df$rt$intType())
  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$Y())
  ensures acc(p$c$Y$shared(ret), wildcard)
  ensures acc(p$c$Y$unique(ret), write)


method f$createY$TF$T$Unit() returns (ret$0: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var l0$y: Ref
  var l0$ya: Ref
  l0$y := con$c$Y$T$Int$T$Y(df$rt$intToRef(10))
  unfold acc(p$c$Y$shared(l0$y), wildcard)
  unfold acc(p$c$X$shared(l0$y), wildcard)
  l0$ya := l0$y.bf$a
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}