25.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:

• Read-only stream IOS will discard already mapped input up to offset. Any further attempt of mapping data at that area will cause an E_eof exception (for Early Of File ;)).
• Flushing is a no-operation for other kind of IO spaces.