the format of a system file.
System files use four data types: 8-bit characters, 32-bit integers,
the format of a system file.
System files use four data types: 8-bit characters, 32-bit integers,
and 64-bit floating points, called here @code{char}, @code{int32},
@code{int64}, and
@code{flt64}, respectively. Data is not necessarily aligned on a word
and 64-bit floating points, called here @code{char}, @code{int32},
@code{int64}, and
@code{flt64}, respectively. Data is not necessarily aligned on a word