| # lpt1 = # avol0, # lpt4 = # avol0, keyset(gch1) = gc-heap(lpt1, log3), remove-refsize0(istore2) = istore2, remove-refsize0(gstore2) = gstore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(istore2), inv(istore1), inv(gstore2), inv(gstore1 \ ns3), log-group-block(log3, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt4), lpt-leb-size(lpt1), lpt-leb-size(lpt4), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol1 ↓ avol0, istore2 ⊑ istore1, ⌊err1⌋ , ¬ dups(log3), pstate0 = unbuffered → isbuf0, pstate0.index? → pstate0.lnum ∈ istore1, pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0 = unbuffered → bleb1 = nobuffer ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then pstate := unbuffered, isbuf := true, adr0 := adr, m := maxino, log0 := log, ns0 := ns else pstate := ?, isbuf := ?, adr := ?, istore0 := ?, istore := ?, ginval := ?, gstore0 := ?, gstore := ?, log := ?, maxino := ?, ns := ?, adr0 := ?, m := ?, log0 := ?, ns0 := ?⟩ ( adr1 = adr ∧ istore5 = istore0 ∧ istore6 = istore ∧ ns1 = ginval ∧ gstore5 = gstore0 ∧ gstore6 = gstore ∧ log1 = log ∧ m1 = maxino ∧ ns2 = ns ∧ pstate2 = pstate ∧ (isbuf1 ↔ isbuf) ∧ adr2 = adr0 ∧ m0 = m ∧ log2 = log0 ∧ ns4 = ns0 ∧ err1 = err) |
# lpt4 = # avol0, # lpt1 = # avol0, keyset(gch1) = gc-heap(lpt1, log3), remove-refsize0(gstore2) = gstore2, remove-refsize0(istore2) = istore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(gstore1 \ ns3), inv(gstore2), inv(istore1), inv(istore2), log-group-block(log3, lpt1), lpt-free-unref(lpt4), lpt-free-unref(lpt1), lpt-leb-size(lpt4), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol1 ↓ avol0, istore2 ⊑ istore1, ⌊err1⌋ , pstate0 = unbuffered → bleb1 = nobuffer, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0.index? → pstate0.lnum ∈ istore1, pstate0 = unbuffered → isbuf0 ⊦ (⌊err1⌋ ∨ err1 = ESUCCESS) ∧ ⟨err := err1; if err = ESUCCESS then pstate := unbuffered, isbuf := true, adr0 := adr, m := maxino, log0 := log, ns0 := ns else pstate := ?, isbuf := ?, adr := ?, istore0 := ?, istore := ?, ginval := ?, gstore0 := ?, gstore := ?, log := ?, maxino := ?, ns := ?, adr0 := ?, m := ?, log0 := ?, ns0 := ?⟩ ( adr1 = adr ∧ istore5 = istore0 ∧ istore6 = istore ∧ ns1 = ginval ∧ gstore5 = gstore0 ∧ gstore6 = gstore ∧ log1 = log ∧ m1 = maxino ∧ ns2 = ns ∧ pstate2 = pstate ∧ (isbuf1 ↔ isbuf) ∧ adr2 = adr0 ∧ m0 = m ∧ log2 = log0 ∧ ns4 = ns0 ∧ err1 = err), dups(log3)
Used terms: err1