[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,

Specification ebm-vol-refine
asm refinement
   

   export ebm-avol-asm

   import ebm-vol-asm

   using ebm-vol-asm, ebm-avol-asm, 
         ebm-vol-abs

   

   by mapping ebm_vol_recover# → ebm_avol_recover#, ebm_vol_get_volume_size# → ebm_avol_get_volume_size#, 
              ebm_vol_write# → ebm_avol_write#, ebm_vol_read# → ebm_avol_read#, ebm_vol_change# → ebm_avol_change#, 
              ebm_vol_remap# → ebm_avol_remap#, ebm_vol_unmap# → ebm_avol_unmap#, ebm_vol_sync_device# → ebm_avol_sync_device#, 
              ebm_vol_get_page_size# → ebm_avol_get_page_size#, ebm_vol_get_leb_size# → ebm_avol_get_leb_size#, 
              ebm_vol_format# → ebm_avol_format#

   abstraction AVOL = abs(AVOLS[VOLID]);

   
end asm refinement