<<>> <> <> <> <> <<>> TarFileFormat: CEDAR DEFINITIONS ~ { NAMSIZ: NAT ~ 100; -- note: divisible by BYTES[CARD32] TBLOCK: NAT ~ 512; NAME: TYPE ~ PACKED ARRAY [0..NAMSIZ) OF CHAR; OCTAL8: TYPE ~ PACKED ARRAY [0..8) OF CHAR; OCTAL12: TYPE ~ PACKED ARRAY [0..12) OF CHAR; LinkType: TYPE ~ MACHINE DEPENDENT { zero(0), normal(60B), hard(61B), symbolic(62B), (BYTE.LAST) }; Link: TYPE ~ MACHINE DEPENDENT RECORD [ <> bytes: PACKED ARRAY [0..NAMSIZ+4) OF CHAR -- to include padding to a 4-byte boundary ]; Header: TYPE ~ RECORD [ name: NAME, mode: OCTAL8, uid: OCTAL8, gid: OCTAL8, size: OCTAL12, mtime: OCTAL12, chksum: OCTAL8, link: Link -- avoid this! - warning: linkflag has been padded ]; headerBytes: NAT ~ BYTES[Header]; sanityCheck: BOOL[TRUE..TRUE] ~ ( headerBytes <= TBLOCK ); }.