The executor must reject a timestamp whose nanosecond component is not in
[0, 1000000000). File extent is likewise a decoded non-negative st_size.
804def linuxSyscallErrorCodeBytes =
805 (lambda unrestricted code : (family LinuxSyscallErrorCode) .
806 (eliminate
807 LinuxSyscallErrorCode
808 (lambda unrestricted current : (family LinuxSyscallErrorCode) . Bytes)
809 code
810 (branch LinuxSyscallPathEmpty . b"ALPHA-LINUX-001")
811 (branch LinuxSyscallPathContainsNUL . b"ALPHA-LINUX-002")
812 (branch
813 LinuxSyscallRequestedBytesOverflow
814 .
815 b"ALPHA-LINUX-003")
816 (branch LinuxSyscallOffsetOverflow . b"ALPHA-LINUX-004")
817 (branch LinuxSyscallInterrupted . b"ALPHA-LINUX-005")
818 (branch LinuxSyscallKernelFailure . b"ALPHA-LINUX-006")
819 (branch LinuxSyscallReadCountInvalid . b"ALPHA-LINUX-007")
820 (branch LinuxSyscallWriteCountInvalid . b"ALPHA-LINUX-008")
821 (branch LinuxSyscallUnexpectedEOF . b"ALPHA-LINUX-009")
822 (branch
823 LinuxSyscallSeekPositionMismatch
824 .
825 b"ALPHA-LINUX-010")
826 (branch LinuxSyscallExtentOverflow . b"ALPHA-LINUX-011")
827 (branch
828 LinuxSyscallUnexpectedPositiveResult
829 .
830 b"ALPHA-LINUX-012")
831 (branch
832 LinuxSyscallIoctlPayloadInvalid
833 .
834 b"ALPHA-LINUX-013")
835 (branch LinuxSyscallMemoryMapFailed . b"ALPHA-LINUX-014")
836 (branch
837 LinuxSyscallResponseKindMismatch
838 .
839 b"ALPHA-LINUX-015")))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.