[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
apebs,
error-class
,
datasize
with
predicates ubi-io-read-echdr-pre : nat × apebs;
ubi-io-read-vidhdr-pre : nat × apebs;
ubi-io-write-echdr-pre : nat × aecheader × apebs;
ubi-io-write-vidhdr-pre : nat × avidheader × apebs;
ubi-io-read-data-pre : nat × nat × nat × nat × buffer × apebs;
ubi-io-write-data-pre : nat × nat × nat × nat × buffer × apebs;
ubi-io-write-data-wl-pre : nat × nat × buffer × apebs;
ubi-io-erase-pre : nat × apebs;
ubi-io-markbad-pre : nat × apebs;
ubi-io-isbad-pre : nat × apebs;
variables n2 : nat;
axioms read-echdr-pre : ⊦ ubi-io-read-echdr-pre(n, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad;
used for: s;
read-vidhdr-pre : ⊦ ubi-io-read-vidhdr-pre(n, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad;
used for: s;
write-echdr-pre : ⊦ ubi-io-write-echdr-pre(n, aehdr, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad ∧ aehdr.valid? ∧ apebs[n].echdr = empty;
used for: s;
write-vidhdr-pre
: ⊦ ubi-io-write-vidhdr-pre(n, avhdr, apebs)
↔ n < # apebs ∧ ¬ apebs[n].bad ∧ avhdr.valid? ∧ apebs[n].echdr.valid? ∧ apebs[n].vidhdr = empty;
used for: s;
read-data-pre
: ⊦ ubi-io-read-data-pre(n, n0, m0, n1, buf, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad ∧ n0 + n1 ≤ LEB_SIZE ∧ m0 + n1 ≤ # buf;
used for: s;
write-data-pre
: ⊦ ubi-io-write-data-pre(n, n0, n1, n2, buf, apebs)
↔ n < # apebs ∧ ¬ apebs[n].bad ∧ apebs[n].echdr.valid? ∧ apebs[n].vidhdr.valid? ∧ is-aligned(n0, EB_PAGE_SIZE)
∧ is-aligned(n2, EB_PAGE_SIZE) ∧ apebs[n].fill ≤ n0 ∧ n0 + n2 ≤ LEB_SIZE ∧ n1 + n2 ≤ # buf;
used for: s;
write-data-wl-pre
: ⊦ ubi-io-write-data-wl-pre(n, n1, buf, apebs)
↔ n < # apebs ∧ ¬ apebs[n].bad ∧ apebs[n].echdr.valid? ∧ apebs[n].vidhdr.valid? ∧ n1 = align↑(datasize(buf, n1), EB_PAGE_SIZE)
∧ apebs[n].fill = 0 ∧ n1 ≤ LEB_SIZE ∧ n1 ≤ # buf ∧ datasize(buf, n1) ≠ 0;
used for: s;
erase-pre : ⊦ ubi-io-erase-pre(n, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad;
used for: s;
markbad-pre : ⊦ ubi-io-markbad-pre(n, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad;
used for: s;
isbad-pre : ⊦ ubi-io-isbad-pre(n, apebs) ↔ n < # apebs;
used for: s;
end enrich