[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,
asm refinement
export aubi-io-asm
import ubi-io-asm
using ubi-io-asm, aubi-io-asm,
ubi-io-abs
by mapping ubi_io_recovery# → aubi_io_recovery#, ubi_io_read_echdr# → aubi_io_read_echdr#,
ubi_io_write_echdr# → aubi_io_write_echdr#, ubi_io_read_vidhdr# → aubi_io_read_vidhdr#,
ubi_io_write_vidhdr# → aubi_io_write_vidhdr#, ubi_io_read_data# → aubi_io_read_data#,
ubi_io_write_data# → aubi_io_write_data#, ubi_io_write_data_wl# → aubi_io_write_data_wl#,
ubi_io_sync_erase# → aubi_io_sync_erase#, ubi_io_markbad# → aubi_io_markbad#, ubi_io_isbad# → aubi_io_isbad#,
ubi_io_get_blockcount# → aubi_io_get_blockcount#, ubi_io_get_page_size# → aubi_io_get_page_size#,
ubi_io_get_leb_size# → aubi_io_get_leb_size#, ubi_io_format# → aubi_io_format#
abstraction abs(PEBS, APEBS);
end asm refinement