interface.fir.diag.txt

/interface.kt:(84,98): info: Generated Viper text for testProperties:
method f$testProperties$TF$T$Foo$T$Unit(p$foo: Ref) returns (ret$0: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$foo), df$rt$c$Foo())
  requires acc(p$c$Foo$shared(p$foo), wildcard)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var anon$0: Ref
  var l0$x: Ref
  var anon$1: Ref
  var anon$2: Ref
  var anon$3: Ref
  var anon$4: Ref
  anon$0 := ps$public$varProp(p$foo, df$rt$intToRef(0))
  anon$2 := pg$public$varProp(p$foo)
  anon$1 := anon$2
  inhale df$rt$isSubtype(df$rt$typeOf(anon$1), df$rt$intType())
  anon$4 := pg$public$valProp(p$foo)
  anon$3 := anon$4
  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$intType())
  l0$x := sp$plusInts(anon$1, anon$3)
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}

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


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


method ps$public$varProp(this$dispatch: Ref, anon$0: Ref)
  returns (ret: Ref)


/interface.kt:(348,358): info: Generated Viper text for createImpl:
field bf$number: Ref

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


method f$createImpl$TF$T$Unit() returns (ret$0: Ref)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var l0$impl: Ref
  var l0$implField: Ref
  l0$impl := con$c$Impl$T$Int$T$Impl(df$rt$intToRef(-1))
  unfold acc(p$c$Impl$shared(l0$impl), wildcard)
  l0$implField := l0$impl.bf$number
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}

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