1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6typedef 7unsigned 8size_t 9; 10typedef 11int 12ptrdiff_t 13; 14typedef 15unsigned 16wchar_t 17; 18typedef 19signed 20char 21int8_t 22; 23typedef 24short 25int16_t 26; 27typedef 28int 29int32_t 30; 31typedef 32long 33long 34int64_t 35; 36typedef 37unsigned 38char 39uint8_t 40; 41typedef 42unsigned 43short 44uint16_t 45; 46typedef 47unsigned 48int 49uint32_t 50; 51typedef 52unsigned 53long 54long 55uint64_t 56; 57typedef 58int8_t 59int_fast8_t 60; 61typedef 62int 63int_fast16_t 64; 65typedef 66int 67int_fast32_t 68; 69typedef 70int64_t 71int_fast64_t 72; 73typedef 74unsigned 75char 76uint_fast8_t 77; 78typedef 79unsigned 80int 81uint_fast16_t 82; 83typedef 84unsigned 85int 86uint_fast32_t 87; 88typedef 89uint64_t 90uint_fast64_t 91; 92typedef 93long 94intptr_t 95; 96typedef 97unsigned 98long 99uintptr_t 100; 101typedef 102int8_t 103int_least8_t 104; 105typedef 106int16_t 107int_least16_t 108; 109typedef 110int32_t 111int_least32_t 112; 113typedef 114int64_t 115int_least64_t 116; 117typedef 118uint8_t 119uint_least8_t 120; 121typedef 122uint16_t 123uint_least16_t 124; 125typedef 126uint32_t 127uint_least32_t 128; 129typedef 130uint64_t 131uint_least64_t 132; 133typedef 134long 135long 136intmax_t 137; 138typedef 139unsigned 140long 141long 142uintmax_t 143; 144typedef 145uint32_t 146seL4_Word 147; 148typedef 149seL4_Word 150seL4_CPtr 151; 152typedef 153seL4_CPtr 154seL4_ARM_Page 155; 156typedef 157seL4_CPtr 158seL4_ARM_PageTable 159; 160typedef 161seL4_CPtr 162seL4_ARM_PageDirectory 163; 164typedef 165seL4_CPtr 166seL4_ARM_ASIDControl 167; 168typedef 169seL4_CPtr 170seL4_ARM_ASIDPool 171; 172typedef 173struct 174{ 175/* frame registers */ 176seL4_Word 177pc 178, 179sp 180, 181cpsr 182, 183r0 184, 185r1 186, 187r8 188, 189r9 190, 191r10 192, 193r11 194, 195r12 196; 197/* other integer registers */ 198seL4_Word 199r2 200, 201r3 202, 203r4 204, 205r5 206, 207r6 208, 209r7 210, 211r14 212; 213} 214seL4_UserContext 215; 216typedef 217enum 218{ 219seL4_ARM_PageCacheable 220= 2210x01 222, 223seL4_ARM_ParityEnabled 224= 2250x02 226, 227seL4_ARM_Default_VMAttributes 228= 2290x03 230, 231/* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */ 232_enum_pad_seL4_ARM_VMAttributes 233= 234( 2351U 236<< 237( 238( 239sizeof 240( 241int 242) 243* 2448 245) 246- 2471 248) 249) 250, 251} 252seL4_ARM_VMAttributes 253; 254struct 255seL4_MessageInfo 256{ 257uint32_t 258words 259[ 2601 261] 262; 263} 264; 265typedef 266struct 267seL4_MessageInfo 268seL4_MessageInfo_t 269; 270static 271inline 272seL4_MessageInfo_t 273__attribute__ 274( 275( 276__const__ 277) 278) 279seL4_MessageInfo_new 280( 281uint32_t 282label 283, 284uint32_t 285capsUnwrapped 286, 287uint32_t 288extraCaps 289, 290uint32_t 291length 292) 293{ 294seL4_MessageInfo_t 295seL4_MessageInfo 296; 297seL4_MessageInfo 298. 299words 300[ 3010 302] 303= 3040 305; 306seL4_MessageInfo 307. 308words 309[ 3100 311] 312|= 313( 314label 315& 3160xfffff 317) 318<< 31912 320; 321seL4_MessageInfo 322. 323words 324[ 3250 326] 327|= 328( 329capsUnwrapped 330& 3310x7 332) 333<< 3349 335; 336seL4_MessageInfo 337. 338words 339[ 3400 341] 342|= 343( 344extraCaps 345& 3460x3 347) 348<< 3497 350; 351seL4_MessageInfo 352. 353words 354[ 3550 356] 357|= 358( 359length 360& 3610x7f 362) 363<< 3640 365; 366return 367seL4_MessageInfo 368; 369} 370struct 371seL4_CapData 372{ 373uint32_t 374words 375[ 3761 377] 378; 379} 380; 381typedef 382struct 383seL4_CapData 384seL4_CapData_t 385; 386enum 387seL4_CapData_tag 388{ 389seL4_CapData_Badge 390= 3910 392, 393seL4_CapData_Guard 394= 3951 396} 397; 398typedef 399enum 400seL4_CapData_tag 401seL4_CapData_tag_t 402; 403typedef 404enum 405{ 406seL4_SysCall 407= 408- 4091 410, 411seL4_SysReplyWait 412= 413- 4142 415, 416seL4_SysSend 417= 418- 4193 420, 421seL4_SysNBSend 422= 423- 4244 425, 426seL4_SysWait 427= 428- 4295 430, 431seL4_SysReply 432= 433- 4346 435, 436seL4_SysYield 437= 438- 4397 440, 441seL4_SysPoll 442= 443- 4448 445, 446seL4_SysDebugPutChar 447= 448- 4499 450, 451seL4_SysDebugHalt 452= 453- 45410 455, 456seL4_SysDebugCapIdentify 457= 458- 45911 460, 461seL4_SysDebugSnapshot 462= 463- 46412 465, 466_enum_pad_seL4_Syscall_ID 467= 468( 4691U 470<< 471( 472( 473sizeof 474( 475int 476) 477* 4788 479) 480- 4811 482) 483) 484} 485seL4_Syscall_ID 486; 487typedef 488enum 489api_object 490{ 491seL4_UntypedObject 492, 493seL4_TCBObject 494, 495seL4_EndpointObject 496, 497seL4_NotificationObject 498, 499seL4_CapTableObject 500, 501seL4_NonArchObjectTypeCount 502, 503} 504seL4_ObjectType 505; 506typedef 507uint32_t 508api_object_t 509; 510typedef 511enum 512{ 513seL4_NoError 514= 5150 516, 517seL4_InvalidArgument 518, 519seL4_InvalidCapability 520, 521seL4_IllegalOperation 522, 523seL4_RangeError 524, 525seL4_AlignmentError 526, 527seL4_FailedLookup 528, 529seL4_TruncatedMessage 530, 531seL4_DeleteFirst 532, 533seL4_RevokeFirst 534, 535seL4_NotEnoughMemory 536, 537} 538seL4_Error 539; 540enum 541priorityConstants 542{ 543seL4_InvalidPrio 544= 545- 5461 547, 548seL4_MinPrio 549= 5500 551, 552seL4_MaxPrio 553= 554255 555} 556; 557enum 558seL4_MsgLimits 559{ 560seL4_MsgLengthBits 561= 5627 563, 564seL4_MsgExtraCapBits 565= 5662 567} 568; 569typedef 570enum 571{ 572seL4_NoFault 573= 5740 575, 576seL4_CapFault 577, 578seL4_VMFault 579, 580seL4_UnknownSyscall 581, 582seL4_UserException 583, 584_enum_pad_seL4_FaultType 585= 586( 5871U 588<< 589( 590( 591sizeof 592( 593int 594) 595* 5968 597) 598- 5991 600) 601) 602, 603} 604seL4_FaultType 605; 606typedef 607enum 608{ 609seL4_NoFailure 610= 6110 612, 613seL4_InvalidRoot 614, 615seL4_MissingCapability 616, 617seL4_DepthMismatch 618, 619seL4_GuardMismatch 620, 621_enum_pad_seL4_LookupFailureType 622= 623( 6241U 625<< 626( 627( 628sizeof 629( 630int 631) 632* 6338 634) 635- 6361 637) 638) 639, 640} 641seL4_LookupFailureType 642; 643typedef 644enum 645{ 646seL4_CanWrite 647= 6480x01 649, 650seL4_CanRead 651= 6520x02 653, 654seL4_CanGrant 655= 6560x04 657, 658seL4_AllRights 659= 6600x07 661, 662/* seL4_CanWrite | seL4_CanRead | seL4_CanGrant */ 663seL4_Transfer_Mint 664= 6650x100 666, 667_enum_pad_seL4_CapRights 668= 669( 6701U 671<< 672( 673( 674sizeof 675( 676int 677) 678* 6798 680) 681- 6821 683) 684) 685, 686} 687seL4_CapRights 688; 689typedef 690struct 691seL4_IPCBuffer_ 692{ 693seL4_MessageInfo_t 694tag 695; 696seL4_Word 697msg 698[ 699120 700] 701; 702seL4_Word 703userData 704; 705seL4_Word 706caps_or_badges 707[ 708( 709( 7101ul 711<< 712( 713seL4_MsgExtraCapBits 714) 715) 716- 7171 718) 719] 720; 721seL4_CPtr 722receiveCNode 723; 724seL4_CPtr 725receiveIndex 726; 727seL4_Word 728receiveDepth 729; 730} 731seL4_IPCBuffer 732; typedef 733seL4_CPtr 734seL4_CNode 735; 736typedef 737seL4_CPtr 738seL4_IRQHandler 739; 740typedef 741seL4_CPtr 742seL4_IRQControl 743; 744typedef 745seL4_CPtr 746seL4_TCB 747; 748typedef 749seL4_CPtr 750seL4_Untyped 751; 752typedef 753seL4_CPtr 754seL4_DomainSet 755; 756typedef 757enum 758_object 759{ 760seL4_ARM_SmallPageObject 761= 762seL4_NonArchObjectTypeCount 763, 764seL4_ARM_LargePageObject 765, 766seL4_ARM_SectionObject 767, 768seL4_ARM_SuperSectionObject 769, 770seL4_ARM_PageTableObject 771, 772seL4_ARM_PageDirectoryObject 773, 774seL4_ObjectTypeCount 775} 776seL4_ArchObjectType 777; 778typedef 779uint32_t 780object_t 781; 782enum 783invocation_label 784{ 785InvalidInvocation 786, 787UntypedRetype 788, 789TCBReadRegisters 790, 791TCBWriteRegisters 792, 793TCBCopyRegisters 794, 795TCBConfigure 796, 797TCBSetPriority 798, 799TCBSetIPCBuffer 800, 801TCBSetSpace 802, 803TCBSuspend 804, 805TCBResume 806, 807TCBBindNotification 808, 809TCBUnbindNotification 810, 811CNodeRevoke 812, 813CNodeDelete 814, 815CNodeRecycle 816, 817CNodeCopy 818, 819CNodeMint 820, 821CNodeMove 822, 823CNodeMutate 824, 825CNodeRotate 826, 827CNodeSaveCaller 828, 829IRQIssueIRQHandler 830, 831IRQInterruptControl 832, 833IRQAckIRQ 834, 835IRQSetIRQHandler 836, 837IRQClearIRQHandler 838, 839DomainSetSet 840, 841nInvocationLabels 842} 843; 844enum 845arch_invocation_label 846{ 847ARMPDClean_Data 848= 849nInvocationLabels 850+ 8510 852, 853ARMPDInvalidate_Data 854= 855nInvocationLabels 856+ 8571 858, 859ARMPDCleanInvalidate_Data 860= 861nInvocationLabels 862+ 8632 864, 865ARMPDUnify_Instruction 866= 867nInvocationLabels 868+ 8693 870, 871ARMPageTableMap 872= 873nInvocationLabels 874+ 8754 876, 877ARMPageTableUnmap 878= 879nInvocationLabels 880+ 8815 882, 883ARMPageMap 884= 885nInvocationLabels 886+ 8876 888, 889ARMPageRemap 890= 891nInvocationLabels 892+ 8937 894, 895ARMPageUnmap 896= 897nInvocationLabels 898+ 8998 900, 901ARMPageClean_Data 902= 903nInvocationLabels 904+ 9059 906, 907ARMPageInvalidate_Data 908= 909nInvocationLabels 910+ 91110 912, 913ARMPageCleanInvalidate_Data 914= 915nInvocationLabels 916+ 91711 918, 919ARMPageUnify_Instruction 920= 921nInvocationLabels 922+ 92312 924, 925ARMPageGetAddress 926= 927nInvocationLabels 928+ 92913 930, 931ARMASIDControlMakePool 932= 933nInvocationLabels 934+ 93514 936, 937ARMASIDPoolAssign 938= 939nInvocationLabels 940+ 94115 942, 943nArchInvocationLabels 944} 945; 946enum 947{ 948seL4_GlobalsFrame 949= 9500xffffc000 951, 952} 953; 954static 955inline 956void 957seL4_Notify 958( 959seL4_CPtr 960dest 961, 962seL4_Word 963msg 964) 965{ 966register 967seL4_Word 968destptr 969asm 970( 971"r0" 972) 973= 974( 975seL4_Word 976) 977dest 978; 979register 980seL4_Word 981info 982asm 983( 984"r1" 985) 986= 987seL4_MessageInfo_new 988( 9890 990, 9910 992, 9930 994, 9951 996) 997. 998words 999[ 10000 1001] 1002; 1003register 1004seL4_Word 1005msg0 1006asm 1007( 1008"r2" 1009) 1010= 1011msg 1012; 1013/* Perform the system call. */ 1014register 1015seL4_Word 1016scno 1017asm 1018( 1019"r7" 1020) 1021= 1022seL4_SysSend 1023; 1024asm 1025volatile 1026( 1027"swi %[swi_num]" 1028: 1029"+r" 1030( 1031destptr 1032) 1033, 1034"+r" 1035( 1036msg0 1037) 1038, 1039"+r" 1040( 1041info 1042) 1043: 1044[ 1045swi_num 1046] 1047"i" 1048( 1049( 1050seL4_SysSend 1051) 1052& 10530x00ffffff 1054) 1055, 1056"r" 1057( 1058scno 1059) 1060: 1061"memory" 1062) 1063; 1064} 1065typedef 1066unsigned 1067long 1068__type_uint8_t_size_incorrect 1069[ 1070( 1071sizeof 1072( 1073uint8_t 1074) 1075== 10761 1077) 1078? 10791 1080: 1081- 10821 1083] 1084; 1085typedef 1086unsigned 1087long 1088__type_uint16_t_size_incorrect 1089[ 1090( 1091sizeof 1092( 1093uint16_t 1094) 1095== 10962 1097) 1098? 10991 1100: 1101- 11021 1103] 1104; 1105typedef 1106unsigned 1107long 1108__type_uint32_t_size_incorrect 1109[ 1110( 1111sizeof 1112( 1113uint32_t 1114) 1115== 11164 1117) 1118? 11191 1120: 1121- 11221 1123] 1124; 1125typedef 1126unsigned 1127long 1128__type_uint64_t_size_incorrect 1129[ 1130( 1131sizeof 1132( 1133uint64_t 1134) 1135== 11368 1137) 1138? 11391 1140: 1141- 11421 1143] 1144; 1145typedef 1146unsigned 1147long 1148__type_int_size_incorrect 1149[ 1150( 1151sizeof 1152( 1153int 1154) 1155== 11564 1157) 1158? 11591 1160: 1161- 11621 1163] 1164; 1165typedef 1166unsigned 1167long 1168__type_bool_size_incorrect 1169[ 1170( 1171sizeof 1172( 1173_Bool 1174) 1175== 11761 1177) 1178? 11791 1180: 1181- 11821 1183] 1184; 1185typedef 1186unsigned 1187long 1188__type_seL4_Word_size_incorrect 1189[ 1190( 1191sizeof 1192( 1193seL4_Word 1194) 1195== 11964 1197) 1198? 11991 1200: 1201- 12021 1203] 1204; 1205typedef 1206unsigned 1207long 1208__type_seL4_CapRights_size_incorrect 1209[ 1210( 1211sizeof 1212( 1213seL4_CapRights 1214) 1215== 12164 1217) 1218? 12191 1220: 1221- 12221 1223] 1224; 1225typedef 1226unsigned 1227long 1228__type_seL4_CapData_t_size_incorrect 1229[ 1230( 1231sizeof 1232( 1233seL4_CapData_t 1234) 1235== 12364 1237) 1238? 12391 1240: 1241- 12421 1243] 1244; 1245typedef 1246unsigned 1247long 1248__type_seL4_CPtr_size_incorrect 1249[ 1250( 1251sizeof 1252( 1253seL4_CPtr 1254) 1255== 12564 1257) 1258? 12591 1260: 1261- 12621 1263] 1264; 1265typedef 1266unsigned 1267long 1268__type_seL4_CNode_size_incorrect 1269[ 1270( 1271sizeof 1272( 1273seL4_CNode 1274) 1275== 12764 1277) 1278? 12791 1280: 1281- 12821 1283] 1284; 1285typedef 1286unsigned 1287long 1288__type_seL4_IRQHandler_size_incorrect 1289[ 1290( 1291sizeof 1292( 1293seL4_IRQHandler 1294) 1295== 12964 1297) 1298? 12991 1300: 1301- 13021 1303] 1304; 1305typedef 1306unsigned 1307long 1308__type_seL4_IRQControl_size_incorrect 1309[ 1310( 1311sizeof 1312( 1313seL4_IRQControl 1314) 1315== 13164 1317) 1318? 13191 1320: 1321- 13221 1323] 1324; 1325typedef 1326unsigned 1327long 1328__type_seL4_TCB_size_incorrect 1329[ 1330( 1331sizeof 1332( 1333seL4_TCB 1334) 1335== 13364 1337) 1338? 13391 1340: 1341- 13421 1343] 1344; 1345typedef 1346unsigned 1347long 1348__type_seL4_Untyped_size_incorrect 1349[ 1350( 1351sizeof 1352( 1353seL4_Untyped 1354) 1355== 13564 1357) 1358? 13591 1360: 1361- 13621 1363] 1364; 1365typedef 1366unsigned 1367long 1368__type_seL4_DomainSet_size_incorrect 1369[ 1370( 1371sizeof 1372( 1373seL4_DomainSet 1374) 1375== 13764 1377) 1378? 13791 1380: 1381- 13821 1383] 1384; 1385typedef 1386unsigned 1387long 1388__type_seL4_ARM_VMAttributes_size_incorrect 1389[ 1390( 1391sizeof 1392( 1393seL4_ARM_VMAttributes 1394) 1395== 13964 1397) 1398? 13991 1400: 1401- 14021 1403] 1404; 1405typedef 1406unsigned 1407long 1408__type_seL4_ARM_Page_size_incorrect 1409[ 1410( 1411sizeof 1412( 1413seL4_ARM_Page 1414) 1415== 14164 1417) 1418? 14191 1420: 1421- 14221 1423] 1424; 1425typedef 1426unsigned 1427long 1428__type_seL4_ARM_PageTable_size_incorrect 1429[ 1430( 1431sizeof 1432( 1433seL4_ARM_PageTable 1434) 1435== 14364 1437) 1438? 14391 1440: 1441- 14421 1443] 1444; 1445typedef 1446unsigned 1447long 1448__type_seL4_ARM_PageDirectory_size_incorrect 1449[ 1450( 1451sizeof 1452( 1453seL4_ARM_PageDirectory 1454) 1455== 14564 1457) 1458? 14591 1460: 1461- 14621 1463] 1464; 1465typedef 1466unsigned 1467long 1468__type_seL4_ARM_ASIDControl_size_incorrect 1469[ 1470( 1471sizeof 1472( 1473seL4_ARM_ASIDControl 1474) 1475== 14764 1477) 1478? 14791 1480: 1481- 14821 1483] 1484; 1485typedef 1486unsigned 1487long 1488__type_seL4_ARM_ASIDPool_size_incorrect 1489[ 1490( 1491sizeof 1492( 1493seL4_ARM_ASIDPool 1494) 1495== 14964 1497) 1498? 14991 1500: 1501- 15021 1503] 1504; 1505typedef 1506unsigned 1507long 1508__type_seL4_UserContext_size_incorrect 1509[ 1510( 1511sizeof 1512( 1513seL4_UserContext 1514) 1515== 151668 1517) 1518? 15191 1520: 1521- 15221 1523] 1524; 1525struct 1526seL4_ARM_Page_GetAddress 1527{ 1528int 1529error 1530; 1531seL4_Word 1532paddr 1533; 1534} 1535; 1536typedef 1537struct 1538seL4_ARM_Page_GetAddress 1539seL4_ARM_Page_GetAddress_t 1540; 1541enum 1542{ 1543seL4_CapNull 1544= 15450 1546, 1547/* null cap */ 1548seL4_CapInitThreadTCB 1549= 15501 1551, 1552/* initial thread's TCB cap */ 1553seL4_CapInitThreadCNode 1554= 15552 1556, 1557/* initial thread's root CNode cap */ 1558seL4_CapInitThreadPD 1559= 15603 1561, 1562/* initial thread's PD cap */ 1563seL4_CapIRQControl 1564= 15654 1566, 1567/* global IRQ controller cap */ 1568seL4_CapASIDControl 1569= 15705 1571, 1572/* global ASID controller cap */ 1573seL4_CapInitThreadASIDPool 1574= 15756 1576, 1577/* initial thread's ASID pool cap */ 1578seL4_CapIOPort 1579= 15807 1581, 1582/* global IO port cap (null cap if not supported) */ 1583seL4_CapIOSpace 1584= 15858 1586, 1587/* global IO space cap (null cap if no IOMMU support) */ 1588seL4_CapBootInfoFrame 1589= 15909 1591, 1592/* bootinfo frame cap */ 1593seL4_CapInitThreadIPCBuffer 1594= 159510 1596, 1597/* initial thread's IPC buffer frame cap */ 1598seL4_CapDomain 1599= 160011 1601/* global domain controller cap */ 1602} 1603; 1604typedef 1605struct 1606{ 1607seL4_Word 1608start 1609; 1610/* first CNode slot position OF region */ 1611seL4_Word 1612end 1613; 1614/* first CNode slot position AFTER region */ 1615} 1616seL4_SlotRegion 1617; 1618typedef 1619struct 1620{ 1621seL4_Word 1622basePaddr 1623; 1624/* base physical address of device region */ 1625seL4_Word 1626frameSizeBits 1627; 1628/* size (2^n bytes) of a device-region frame */ 1629seL4_SlotRegion 1630frames 1631; 1632/* device-region frame caps */ 1633} 1634seL4_DeviceRegion 1635; 1636typedef 1637struct 1638{ 1639seL4_Word 1640nodeID 1641; 1642/* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */ 1643seL4_Word 1644numNodes 1645; 1646/* number of seL4 nodes (1 if uniprocessor) */ 1647seL4_Word 1648numIOPTLevels 1649; 1650/* number of IOMMU PT levels (0 if no IOMMU support) */ 1651seL4_IPCBuffer 1652* 1653ipcBuffer 1654; 1655/* pointer to initial thread's IPC buffer */ 1656seL4_SlotRegion 1657empty 1658; 1659/* empty slots (null caps) */ 1660seL4_SlotRegion 1661sharedFrames 1662; 1663/* shared-frame caps (shared between seL4 nodes) */ 1664seL4_SlotRegion 1665userImageFrames 1666; 1667/* userland-image frame caps */ 1668seL4_SlotRegion 1669userImagePTs 1670; 1671/* userland-image PT caps */ 1672seL4_SlotRegion 1673untyped 1674; 1675/* untyped-object caps (untyped caps) */ 1676seL4_Word 1677untypedPaddrList 1678[ 1679167 1680] 1681; 1682/* physical address of each untyped cap */ 1683uint8_t 1684untypedSizeBitsList 1685[ 1686167 1687] 1688; 1689/* size (2^n) bytes of each untyped cap */ 1690uint8_t 1691initThreadCNodeSizeBits 1692; 1693/* initial thread's root CNode size (2^n slots) */ 1694seL4_Word 1695numDeviceRegions 1696; 1697/* number of device regions */ 1698seL4_DeviceRegion 1699deviceRegions 1700[ 1701199 1702] 1703; 1704/* device regions */ 1705uint8_t 1706initThreadDomain 1707; 1708/* Initial thread's domain ID */ 1709} 1710seL4_BootInfo 1711; 1712int 1713EventFrom__run 1714( 1715void 1716) 1717{ 1718/* Nothing required. */ 1719return 17200 1721; 1722} 1723void 1724EventFrom_emit_underlying 1725( 1726void 1727) 1728{ 1729seL4_Notify 1730( 17316 1732, 1733/* ignored */ 17340 1735) 1736; 1737} 1738