[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 awbuf-asm
import wbuf-asm
using wbuf-asm, awbuf-asm,
wbuf-abs
by mapping wbuf_recover# → awbuf_recover#, wbuf_get_volume_size# → awbuf_get_volume_size#, wbuf_get_buf# → awbuf_get_buf#,
wbuf_is_readonly# → awbuf_is_readonly#, wbuf_enter_readonly# → awbuf_enter_readonly#,
wbuf_move_buf# → awbuf_move_buf#, wbuf_destroy_buf# → awbuf_destroy_buf#, wbuf_write_buf# → awbuf_write_buf#,
wbuf_commit# → awbuf_commit#, wbuf_requires_commit# → awbuf_requires_commit#,
wbuf_add_log_leb# → awbuf_add_log_leb#, wbuf_read_buf# → awbuf_read_buf#, wbuf_remap# → awbuf_remap#,
wbuf_unmap# → awbuf_unmap#, wbuf_get_page_size# → awbuf_get_page_size#, wbuf_get_leb_size# → awbuf_get_leb_size#,
wbuf_format# → awbuf_format#
abstraction abs(WVOL, BUFLEB, WBUF, PVOL, ROFS) ∧ WBUFLEB = BUFLEB ∧ WROOTADR = PROOTADR ∧ WMAXINO = PMAXINO ∧ WLOG = PLOG ∧ WLPT = PLPT
∧ WORPHANS = PORPHANS ∧ (AROFS ↔ ROFS)
;
end asm refinement