whileok.vpr

field val_bool: Bool

field val_int: Int

field val_ref: Ref

function read$(): Perm
  ensures none < result
  ensures result < write


predicate bool(self: Ref) {
  acc(self.val_bool, write)
}

predicate isize(self: Ref) {
  acc(self.val_int, write)
}

predicate tuple0$(self: Ref) {
  true
}

method whileok() returns (_0: Ref)
{
  var __t0: Bool
  var __t1: Bool
  var __t2: Bool
  var __t3: Bool
  var __t4: Bool
  var __t5: Bool
  var _1: Ref
  var _2: Ref
  var _3: Ref
  label start
  // ========== start ==========
  
  // Name: "whileok::whileok"
  
  // Def path: "whileok::whileok[0]"
  
  // Span: whileok.rs:3:1: 6:2
  
  __t0 := false
  __t1 := false
  __t2 := false
  __t3 := false
  // Preconditions:
  
  label pre
  goto bb0
  label bb0
  // ========== bb0 ==========
  
  __t0 := true
  // [mir] StorageLive(_1)
  
  // [mir] _1 = const true
  
  _1 := builtin$havoc_ref()
  inhale acc(_1.val_bool, write)
  _1.val_bool := true
  // [mir] goto -> bb1
  
  goto bb0_bb1
  label bb0_bb1
  // ========== bb0 --> bb1 ==========
  
  // Assert and exhale the loop invariant of block bb1
  
  fold acc(bool(_1), write)
  // obtain acc(bool(_1), read)
  
  exhale acc(bool(_1), read$())
  // begin frame
  
  goto bb1
  label bb1
  // ========== bb1 ==========
  
  __t1 := true
  // [mir] switchInt(move _2) -> [false: bb2, otherwise: bb3]
  
  if (__t5) {
    goto bb1_bb2
  }
  goto bb1_bb3
  label bb1_bb2
  // ========== bb1 --> bb2 ==========
  
  // Inhale the loop invariant of block bb1
  
  // end frame
  
  inhale acc(bool(_1), read$())
  
  // [mir] _2 = _1
  
  _2 := builtin$havoc_ref()
  inhale acc(_2.val_bool, write)
  // ERROR: Unfolding bool(_1) might fail. There might be insufficient permission to access bool(_1)
  // Possible cause: when we end the frame, we get back acc(bool(_1), write), and the unfolding in
  // branch_ctx unfolds with maximum permissions.
  // Possible solution: For loop exits, we do not inhale pred-permissions and permissions of fields.
  // Instead, we could rely on `end frame` to inhale the permissions.
  // This solution should change the `inhale acc(bool(_1), read$())` at line 95 into `inhale acc(bool(_1), write)`
  // NOTE: we should also do something similar for loop heads; that is we let the 
  // `begin frame` exhale all the current permissions (line 74 would then become `exhale acc(bool(_1), write)`).
  unfold acc(bool(_1), write)
  _2.val_bool := _1.val_bool
  label l0
  __t4 := _2.val_bool
  inhale !__t4
  goto bb2
  label bb1_bb3
  // ========== bb1 --> bb3 ==========
  
  // Inhale the loop invariant of block bb1
  
  inhale acc(bool(_1), read$())
  inhale true
  inhale true
  
  // [mir] _2 = _1
  
  _2 := builtin$havoc_ref()
  inhale acc(_2.val_bool, write)
  unfold acc(bool(_1), read$())
  _2.val_bool := _1.val_bool
  label l1
  __t4 := _2.val_bool
  inhale __t4
  goto bb3
  label bb2
  // ========== bb2 ==========
  
  __t3 := true
  
  _0 := builtin$havoc_ref()
  inhale acc(tuple0$(_0), write)
  
  // [mir] return
  
  goto return
  label bb3
  // ========== bb3 ==========
  
  __t2 := true
  // [mir] _3 = ()
  
  _3 := builtin$havoc_ref()
  inhale acc(tuple0$(_3), write)
  // [mir] goto -> bb1
  
  goto bb3_bb1
  label bb3_bb1
  // ========== bb3 --> bb1 ==========
  
  // Assert and exhale the loop invariant of block bb1
  
  fold acc(bool(_1), read$())
  // obtain acc(bool(_1), read)
  
  exhale acc(bool(_1), read$())
  goto bb1
  label return
  // ========== return ==========
  
  // Target of any 'return' statement.
  
  // Exhale postcondition
  
  // Fold predicates for &mut args and transfer borrow permissions to old
  
  // Fold the result
  
  // obtain acc(tuple0$(_0), write)
  
  exhale acc(tuple0$(_0), write)
  goto end_of_method
  label end_of_method
}

method builtin$havoc_ref() returns (ret: Ref)