12.3 ios_save_bytes

The function ios_save_bytes saves a range of bytes from an IO space to a file.

It has the following prototype:

fun ios_save_bytes = (int<32> ios, string file,
                      offset<uint<64>,B> from,
                      offset<uint<64>,B> size,
                      int<32> append_p) void

Where ios is the IO space from which save bytes.

file is the name of the file where to save the bytes.

to and size are byte offsets in the IO space determining the range of bytes to save.

By default the output file is truncated if it already exists. If append_p is true, then the data is instead appended at the end of the file.