[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,
data asm specification
aubi_io
using ubi-io-inv
procedures aubi_io_read_echdr# nat × apebs : aecheader : bool × error nondeterministic;
aubi_io_write_echdr# nat × aecheader : apebs : error nondeterministic;
aubi_io_read_vidhdr# nat × apebs : avidheader : bool × error nondeterministic;
aubi_io_write_vidhdr# nat × avidheader : apebs : error nondeterministic;
aubi_io_read_data# nat × nat × nat × nat × apebs : buffer : bool × error nondeterministic;
aubi_io_write_data# nat × nat × nat × nat × buffer : apebs : error nondeterministic;
aubi_io_write_data_wl# nat × nat × buffer : apebs : error nondeterministic;
aubi_io_sync_erase# nat : apebs : error nondeterministic;
aubi_io_markbad# nat : apebs : error nondeterministic;
aubi_io_isbad# nat × apebs : : bool × error nondeterministic;
aubi_io_get_blockcount# apebs : : nat ;
aubi_io_get_page_size# apebs : : nat ;
aubi_io_get_leb_size# apebs : : nat ;
aubi_io_recovery# apebs : nonfunctional ;
aubi_io_format# : : apebs × error nondeterministic;
variables PNUM : nat flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
OFFSET : nat flexible;
ISBAD : bool flexible;
isbad : bool;
ERR : error flexible;
ERR0 : error flexible;
BUF : buffer flexible;
BUF0 : buffer flexible;
APEBS : apebs flexible;
APEBS0 : apebs flexible;
AEHDR : aecheader flexible;
AVHDR : avidheader flexible;
APEB : apeb flexible;
BITFLIPS : bool flexible;
bitflips : bool;
state variables APEBS : apebs flexible;
initialization procedure aubi_io_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ ubi-io-inv(APEBS);
crash predicate APEBS = APEBS`
with crash-neutrality
recovery procedure aubi_io_recovery#
declarations read-echdr:
aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR)
precondition ubi-io-read-echdr-pre(PNUM, APEBS);
postcondition true;
{if ubi-io-read-echdr-pre(PNUM, APEBS)
then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then AEHDR := APEBS[PNUM].echdr else AEHDR := ?}
else abort
}
write-echdr:
aubi_io_write_echdr#(PNUM, AEHDR; APEBS; ERR)
precondition ubi-io-write-echdr-pre(PNUM, AEHDR, APEBS);
postcondition true;
{if ubi-io-write-echdr-pre(PNUM, AEHDR, APEBS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then APEBS[PNUM].echdr := AEHDR else choose AEHDR with ¬ AEHDR.valid? in APEBS[PNUM].echdr := AEHDR}
else abort
}
read-vidhdr:
aubi_io_read_vidhdr#(PNUM, APEBS; AVHDR; BITFLIPS, ERR)
precondition ubi-io-read-vidhdr-pre(PNUM, APEBS);
postcondition true;
{if ubi-io-read-vidhdr-pre(PNUM, APEBS)
then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then AVHDR := APEBS[PNUM].vidhdr else AVHDR := ?}
else abort
}
write-vidhdr:
aubi_io_write_vidhdr#(PNUM, AVHDR; APEBS; ERR)
precondition ubi-io-write-vidhdr-pre(PNUM, AVHDR, APEBS);
postcondition true;
{if ubi-io-write-vidhdr-pre(PNUM, AVHDR, APEBS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then APEBS[PNUM].vidhdr := AVHDR else choose AVHDR with ¬ AVHDR.valid? in APEBS[PNUM].vidhdr := AVHDR}
else abort
}
read-data:
aubi_io_read_data#(PNUM, OFFSET, N0, N, APEBS; BUF; BITFLIPS, ERR)
precondition ubi-io-read-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS);
postcondition true;
{if ubi-io-read-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS)
then {fail_or_success#(; ; ERR); BITFLIPS := ?;
if ERR = ESUCCESS
then BUF := copy(APEBS[PNUM].data, OFFSET, BUF, N0, N)
else choose BUF0
with # BUF0 = # BUF ∧ range=(BUF0, 0, BUF, 0, N0) ∧ range=(BUF0, N0 + N, BUF, N0 + N, # BUF - N0 + N)
in BUF := BUF0}
else abort
}
write-data:
aubi_io_write_data#(PNUM, OFFSET, N0, N, BUF; APEBS; ERR)
precondition ubi-io-write-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS);
postcondition true;
{if ubi-io-write-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then APEBS[PNUM]
:= mkpeb
(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr,
subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - OFFSET - N), OFFSET + N,
APEBS[PNUM].bad)
else choose N1
with (N1 < N ∨ N1 = 0 ∧ N = 0) ∧ is-aligned(N1, EB_PAGE_SIZE)
in if N1 ≠ 0
then APEBS[PNUM]
:= mkpeb
(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr,
subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N1) + mkempbuf(LEB_SIZE - OFFSET - N1), OFFSET + N1,
APEBS[PNUM].bad)}
else abort
}
write-data-wl:
aubi_io_write_data_wl#(PNUM, N, BUF; APEBS; ERR)
precondition ubi-io-write-data-wl-pre(PNUM, N, BUF, APEBS);
postcondition true;
{if ubi-io-write-data-wl-pre(PNUM, N, BUF, APEBS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then APEBS[PNUM]
:= mkpeb(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(BUF, 0, N) + mkempbuf(LEB_SIZE - N), N, APEBS[PNUM].bad)
else choose BUF0
with # BUF0 ≤ N ∧ is-aligned(# BUF0, EB_PAGE_SIZE)
∧ ( datasize(BUF0, # BUF0) < datasize(BUF, N)
∨ checksum(BUF0 + mkempbuf(N - # BUF0), datasize(BUF, N)) ≠ checksum(BUF, datasize(BUF, N)))
in APEBS[PNUM]
:= mkpeb(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, BUF0 + mkempbuf(LEB_SIZE - # BUF0), # BUF0, APEBS[PNUM].bad)}
else abort
}
sync-erase:
aubi_io_sync_erase#(PNUM; APEBS; ERR)
precondition ubi-io-erase-pre(PNUM, APEBS);
postcondition true;
{if ubi-io-erase-pre(PNUM, APEBS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then APEBS[PNUM] := mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)
else {choose APEB with ubi-io-peb-inv(APEB) ∧ ¬ APEB.bad ∧ ¬ APEB.vidhdr.valid? in APEBS[PNUM] := APEB or skip}}
else abort
}
markbad:
aubi_io_markbad#(PNUM; APEBS; ERR)
precondition ubi-io-markbad-pre(PNUM, APEBS);
postcondition true;
{if ubi-io-markbad-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM].bad := true} else abort
}
isbad:
aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR)
precondition ubi-io-isbad-pre(PNUM, APEBS);
postcondition true;
{if ubi-io-isbad-pre(PNUM, APEBS)
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISBAD := APEBS[PNUM].bad else ISBAD := ?}
else abort
}
get-blockcount:aubi_io_get_blockcount#(APEBS; ; N) precondition true; postcondition true;{N := # APEBS}
get-page-size:aubi_io_get_page_size#(APEBS; ; N) precondition true; postcondition true;{N := EB_PAGE_SIZE}
get-leb-size:aubi_io_get_leb_size#(APEBS; ; N) precondition true; postcondition true;{N := LEB_SIZE}
recovery:aubi_io_recovery#(APEBS) precondition true; postcondition true;{skip}
format:
aubi_io_format#(; ; APEBS, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then choose APEBS0 with ubi-io-initial(APEBS0) in APEBS := APEBS0 else APEBS := ?}
}
end data asm specification