24.16.5.3 Unbounded array maps ¶

We mentioned above that if an end-of-file condition happens while performing a mapping (be it bounded by number of elements or bounded by size) an EOF exception is raised, and the mapping operation is aborted.

Unbounded array mappings are performed by using an unbounded array type in the mapping operation, like in:

type[] @ 0#B

The above construction will map values of type type in the IO space until there is an end-of-file condition, or a constraint fails, whatever happens first. When it is a constraint expression that fails, that last element is not included in the mapped array.

Let’s assume a binary file contains a series of blocks, located one after the other, of a kind described by the following struct type:

type Block =
  struct
  {
     byte magic[2] : magic[0] == 'B' && magic[1] == 'K';
     ... other data ...
  };

we can map the blocks using an unbounded array map:

(poke) Block[] @ 0#B
[ ... blocks ... ]

If the blocks extend up to the end of the IO space, that many blocks will be mapped. If there is some other content in the file following the blocks, the constraint in the magic field will fail and will delimit the map that way (provided the binary format is well designed.)