1340def linuxAcceptExtendedResponse =
1341 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1342 (lambda unrestricted request : (family LinuxExtendedSyscallRequest) .
1343 (lambda unrestricted response : (family LinuxExtendedSyscallResponse) .
1344 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1345 (eliminate
1346 LinuxExtendedSyscallRequest
1347 (lambda unrestricted current : (family LinuxExtendedSyscallRequest) .
1348 (family LinuxSyscallReceiptDecision))
1349 request
1350 (branch
1351 LinuxFstatRequest
1352 descriptor
1353 .
1354 (eliminate
1355 LinuxExtendedSyscallResponse
1356 (lambda unrestricted current : (family LinuxExtendedSyscallResponse) .
1357 (family LinuxSyscallReceiptDecision))
1358 response
1359 (branch LinuxFstatSucceeded status . (linuxAcceptExtendedSuccess response audit))
1360 (branch
1361 LinuxClockGettimeSucceeded
1362 timestamp
1363 .
1364 (linuxRejectReceipt
1365 (constructor LinuxSyscallContractErrorCode LinuxReceiptExtendedKindMismatch)
1366 audit))
1367 (branch
1368 LinuxExtendedSyscallFailed
1369 error
1370 errno
1371 .
1372 (nat-eliminate
1373 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1374 (constructor
1375 LinuxSyscallReceiptDecision
1376 LinuxSyscallReceiptFailed
1377 error
1378 errno
1379 audit)
1380 (lambda unrestricted interruptedPredecessor : Nat .
1381 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1382 (constructor
1383 LinuxSyscallReceiptDecision
1384 LinuxSyscallReceiptRetryInterrupted
1385 invocation
1386 audit)))
1387 (linuxErrnoIsInterrupted errno)))))
1388 (branch
1389 LinuxClockGettimeRequest
1390 clock
1391 .
1392 (eliminate
1393 LinuxExtendedSyscallResponse
1394 (lambda unrestricted current : (family LinuxExtendedSyscallResponse) .
1395 (family LinuxSyscallReceiptDecision))
1396 response
1397 (branch
1398 LinuxFstatSucceeded
1399 status
1400 .
1401 (linuxRejectReceipt
1402 (constructor LinuxSyscallContractErrorCode LinuxReceiptExtendedKindMismatch)
1403 audit))
1404 (branch
1405 LinuxClockGettimeSucceeded
1406 timestamp
1407 .
1408 (linuxAcceptExtendedSuccess response audit))
1409 (branch
1410 LinuxExtendedSyscallFailed
1411 error
1412 errno
1413 .
1414 (nat-eliminate
1415 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1416 (constructor
1417 LinuxSyscallReceiptDecision
1418 LinuxSyscallReceiptFailed
1419 error
1420 errno
1421 audit)
1422 (lambda unrestricted interruptedPredecessor : Nat .
1423 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1424 (constructor
1425 LinuxSyscallReceiptDecision
1426 LinuxSyscallReceiptRetryInterrupted
1427 invocation
1428 audit)))
1429 (linuxErrnoIsInterrupted errno))))))))))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.