flush
The builtin flush
performs a “flushing” operation on a given
IO space. The prototype is:
fun flush = (int<32> ios, offset<uint<64>,1> offset) void
Where ios is the IOS identifier where to perform the flush. The semantics associated with the “flushing” operation depends on the kind of IO space: