Proof step 196 from proof write-term (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 197:

  files0[m] = mkfile(m2, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content), err = err1, err1 = ESUCCESS, files = files1, m2 < m0 + ino, afs-cons(dirs, files0[m, mkfile(m2, md0, # links(m, dirs), content0 upto m2)]), afs-cons(dirs, files0), of-cons(of, dirs, files0), m ∈ files1, fd ∈ of, m ∈ files0, n ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪err := err0; choose bv with true in asynced := bv; dirs0 := dirs; err1 := err; if err1 = ESUCCESS then afs_write_inode#(mkinode(m, md0, false, # links(m, dirs), 0, m0 + ino); err1, dirs, files1; asynced); if err1 ≠ ESUCCESS then ino := (m0 ≤ m2 ⊃ m2 - m0;0), err1 := ESUCCESS; of[fd].pos := m0 + ino⟫ (dirs0 = dirs), ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0

• Proof step 233:

  files0[m] = mkfile(m2, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content), err = err0, err0 = ESUCCESS, files = files1, m2 < m0 + ino, afs-cons(dirs, files0[m, mkfile(m2, md0, # links(m, dirs), content0 upto m2)]), afs-cons(dirs, files0), of-cons(of, dirs, files0), m ∈ files1, fd ∈ of, m ∈ files0, n ≤ # buf0 ⊦ ino = 0, n = 0, ∃ err0. ⌊err0⌋ ∨ err0 = ESUCCESS, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0

Rule argument

Additional information