| persistence_read_gblock_nodes#(LNUM, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ADRLIST, NODELIST; ERR) {if LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ (∃ gndx, lax. abs-nodes(WVOL[LNUM].data, gndx, lax, true)) then let BUF = mkbuf(LEBSIZE), OFFSET = 0 in {awbuf_read_buf#(LNUM, 0, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR); while ERR = ESUCCESS ∧ OFFSET < LEBSIZE do {/* (inv-read-gblock-nodes : invariant (ERR = ESUCCESS ∨ ERR = ENOENT ∨ ⌊ERR⌋ ) ∧ ( ERR = ESUCCESS ∨ ERR = ENOENT → read-gblock-inv(LNUM, OFFSET, ADRLIST, NODELIST, ADRLIST`, NODELIST`, WVOL[LNUM].data, ERR = ENOENT)) wfbound (ERR ≠ ESUCCESS ⊃ 0;LEBSIZE - OFFSET)) */; if ¬ OFFSET + NODE_HEADER_SIZE ≤ # BUF ∨ isempty(BUF, OFFSET, NODE_HEADER_SIZE) then ERR := ENOENT else let NDHD = ? in {decode_header#(OFFSET, BUF; NDHD; ERR); if ERR ≠ ESUCCESS then debug# ("persistence: read_gblock_nodes could not decode header in LEB " + LNUM.toString + " at offset " + OFFSET.toString) else let SIZE = 2 * NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE) in {if OFFSET + SIZE > LEBSIZE then {debug# ( "persistence: read_gblock_nodes ignoring node of size " + SIZE.toString + " at offset " + OFFSET.toString + " in LEB " + LNUM.toString); ERR := ENOENT} else if ¬ range= (BUF, OFFSET + NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) then {ERR := ENOENT; debug# ("persistence: read_gblock_nodes partial node at offset " + OFFSET.toString + " in LEB " + LNUM.toString)} else if ¬ NDHD.ispadding then let GND = ? in {decode_group_node#(OFFSET, SIZE, BUF; GND; ERR); if ERR ≠ ESUCCESS then debug# ( "persistence: read_gblock_nodes could not decode node at offset " + OFFSET.toString + " in LEB " + LNUM.toString) else {NODELIST := NODELIST + GND; ADRLIST := ADRLIST + @(LNUM, OFFSET, SIZE)}}; if ERR = ESUCCESS then OFFSET := OFFSET + SIZE}}}; if ERR = ENOENT then ERR := ESUCCESS} else abort } |