manual_permissions.fir.diag.txt

/manual_permissions.kt:(145,176): info: Generated Viper text for testManualPermissionFieldGetter:
field bf$a: Ref

field bf$b: Ref

method f$testManualPermissionFieldGetter$TF$T$ManualPermissionFields$T$Unit(p$mpf: Ref)
  returns (ret$0: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$mpf), df$rt$c$ManualPermissionFields())
  requires acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  var l0$a: Ref
  var l0$b: Ref
  unfold acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
  l0$a := p$mpf.bf$a
  l0$b := p$mpf.bf$b
  inhale df$rt$isSubtype(df$rt$typeOf(l0$b), df$rt$intType())
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}

/manual_permissions.kt:(251,282): info: Generated Viper text for testManualPermissionFieldSetter:
field bf$a: Ref

field bf$b: Ref

method f$testManualPermissionFieldSetter$TF$T$ManualPermissionFields$T$Unit(p$mpf: Ref)
  returns (ret$0: Ref)
  requires df$rt$isSubtype(df$rt$typeOf(p$mpf), df$rt$c$ManualPermissionFields())
  requires acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
{
  p$mpf.bf$b := df$rt$intToRef(123)
  label lbl$ret$0
  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
}