21.16.1.5 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: