1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7void abort(void); 8typedef unsigned wchar_t; 9typedef unsigned int size_t; 10typedef int ptrdiff_t; 11typedef unsigned int uintptr_t; 12typedef int intptr_t; 13typedef signed char int8_t; 14typedef short int16_t; 15typedef int int32_t; 16typedef long long int64_t; 17typedef long long intmax_t; 18typedef unsigned char uint8_t; 19typedef unsigned short uint16_t; 20typedef unsigned int uint32_t; 21typedef unsigned long long uint64_t; 22typedef unsigned long long uintmax_t; 23typedef int8_t int_fast8_t; 24typedef int64_t int_fast64_t; 25typedef int8_t int_least8_t; 26typedef int16_t int_least16_t; 27typedef int32_t int_least32_t; 28typedef int64_t int_least64_t; 29typedef uint8_t uint_fast8_t; 30typedef uint64_t uint_fast64_t; 31typedef uint8_t uint_least8_t; 32typedef uint16_t uint_least16_t; 33typedef uint32_t uint_least32_t; 34typedef uint64_t uint_least64_t; 35typedef int32_t int_fast16_t; 36typedef int32_t int_fast32_t; 37typedef uint32_t uint_fast16_t; 38typedef uint32_t uint_fast32_t; 39typedef uint32_t seL4_Word; 40typedef seL4_Word seL4_CPtr; 41typedef seL4_CPtr seL4_ARM_Page; 42typedef seL4_CPtr seL4_ARM_PageTable; 43typedef seL4_CPtr seL4_ARM_PageDirectory; 44typedef seL4_CPtr seL4_ARM_ASIDControl; 45typedef seL4_CPtr seL4_ARM_ASIDPool; 46typedef struct seL4_UserContext_ { 47 /* frame registers */ 48 seL4_Word pc, sp, cpsr, r0, r1, r8, r9, r10, r11, r12; 49 /* other integer registers */ 50 seL4_Word r2, r3, r4, r5, r6, r7, r14; 51} seL4_UserContext; 52typedef enum { 53 seL4_ARM_PageCacheable = 0x01, 54 seL4_ARM_ParityEnabled = 0x02, 55 seL4_ARM_Default_VMAttributes = 0x03, 56 seL4_ARM_ExecuteNever = 0x04, 57 /* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */ 58 _enum_pad_seL4_ARM_VMAttributes = (1U << ((sizeof(int) * 8) - 1)) - 1, 59} seL4_ARM_VMAttributes; 60struct seL4_MessageInfo { 61 uint32_t words[1]; 62}; 63typedef struct seL4_MessageInfo seL4_MessageInfo_t; 64static inline seL4_MessageInfo_t __attribute__((__const__)) 65seL4_MessageInfo_new(uint32_t label, uint32_t capsUnwrapped, uint32_t extraCaps, 66 uint32_t length) { 67 seL4_MessageInfo_t seL4_MessageInfo; 68 seL4_MessageInfo.words[0] = 0; 69 /* fail if user has passed bits that we will override */ 70 (void)0; 71 seL4_MessageInfo.words[0] |= (label & 0xfffff) << 12; 72 /* fail if user has passed bits that we will override */ 73 (void)0; 74 seL4_MessageInfo.words[0] |= (capsUnwrapped & 0x7) << 9; 75 /* fail if user has passed bits that we will override */ 76 (void)0; 77 seL4_MessageInfo.words[0] |= (extraCaps & 0x3) << 7; 78 /* fail if user has passed bits that we will override */ 79 (void)0; 80 seL4_MessageInfo.words[0] |= (length & 0x7f) << 0; 81 return seL4_MessageInfo; 82} 83static inline uint32_t __attribute__((__const__)) 84seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo) { 85 return (seL4_MessageInfo.words[0] & 0x7f) >> 0; 86} 87struct seL4_CapData { 88 uint32_t words[1]; 89}; 90typedef struct seL4_CapData seL4_CapData_t; 91enum seL4_CapData_tag { seL4_CapData_Badge = 0, seL4_CapData_Guard = 1 }; 92typedef enum seL4_CapData_tag seL4_CapData_tag_t; 93typedef enum { 94 seL4_SysCall = -1, 95 seL4_SysReplyWait = -2, 96 seL4_SysSend = -3, 97 seL4_SysNBSend = -4, 98 seL4_SysWait = -5, 99 seL4_SysReply = -6, 100 seL4_SysYield = -7, 101 seL4_SysDebugPutChar = -8, 102 seL4_SysDebugHalt = -9, 103 seL4_SysDebugCapIdentify = -10, 104 seL4_SysDebugSnapshot = -11, 105 _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int) * 8) - 1)) - 1 106} seL4_Syscall_ID; 107typedef enum api_object { 108 seL4_UntypedObject, 109 seL4_TCBObject, 110 seL4_EndpointObject, 111 seL4_AsyncEndpointObject, 112 seL4_CapTableObject, 113 seL4_NonArchObjectTypeCount, 114} seL4_ObjectType; 115typedef uint32_t api_object_t; 116typedef enum { 117 seL4_NoError = 0, 118 seL4_InvalidArgument, 119 seL4_InvalidCapability, 120 seL4_IllegalOperation, 121 seL4_RangeError, 122 seL4_AlignmentError, 123 seL4_FailedLookup, 124 seL4_TruncatedMessage, 125 seL4_DeleteFirst, 126 seL4_RevokeFirst, 127 seL4_NotEnoughMemory, 128} seL4_Error; 129enum priorityConstants { 130 seL4_InvalidPrio = -1, 131 seL4_MinPrio = 0, 132 seL4_MaxPrio = 255 133}; 134enum seL4_MsgLimits { seL4_MsgLengthBits = 7, seL4_MsgExtraCapBits = 2 }; 135enum { 136 seL4_MsgMaxLength = 120, 137}; 138typedef enum { 139 seL4_NoFault = 0, 140 seL4_CapFault, 141 seL4_VMFault, 142 seL4_UnknownSyscall, 143 seL4_UserException, 144 seL4_Interrupt, 145 _enum_pad_seL4_FaultType = (1U << ((sizeof(int) * 8) - 1)) - 1, 146} seL4_FaultType; 147typedef enum { 148 seL4_NoFailure = 0, 149 seL4_InvalidRoot, 150 seL4_MissingCapability, 151 seL4_DepthMismatch, 152 seL4_GuardMismatch, 153 _enum_pad_seL4_LookupFailureType = (1U << ((sizeof(int) * 8) - 1)) - 1, 154} seL4_LookupFailureType; 155typedef enum { 156 seL4_CanWrite = 0x01, 157 seL4_CanRead = 0x02, 158 seL4_CanGrant = 0x04, 159 seL4_AllRights = 0x07, 160 /* seL4_CanWrite | seL4_CanRead | seL4_CanGrant */ 161 _enum_pad_seL4_CapRights = (1U << ((sizeof(int) * 8) - 1)) - 1, 162} seL4_CapRights; 163typedef struct seL4_IPCBuffer_ { 164 seL4_MessageInfo_t tag; 165 seL4_Word msg[seL4_MsgMaxLength]; 166 seL4_Word userData; 167 seL4_Word caps_or_badges[((1ul << (seL4_MsgExtraCapBits)) - 1)]; 168 seL4_CPtr receiveCNode; 169 seL4_CPtr receiveIndex; 170 seL4_Word receiveDepth; 171} seL4_IPCBuffer; 172typedef seL4_CPtr seL4_CNode; 173typedef seL4_CPtr seL4_IRQHandler; 174typedef seL4_CPtr seL4_IRQControl; 175typedef seL4_CPtr seL4_TCB; 176typedef seL4_CPtr seL4_Untyped; 177typedef seL4_CPtr seL4_DomainSet; 178typedef enum _object { 179 seL4_ARM_SmallPageObject = seL4_NonArchObjectTypeCount, 180 seL4_ARM_LargePageObject, 181 seL4_ARM_SectionObject, 182 seL4_ARM_SuperSectionObject, 183 seL4_ARM_PageTableObject, 184 seL4_ARM_PageDirectoryObject, 185 seL4_ObjectTypeCount 186} seL4_ArchObjectType; 187typedef uint32_t object_t; 188enum invocation_label { 189 InvalidInvocation, 190 UntypedRetype, 191 TCBReadRegisters, 192 TCBWriteRegisters, 193 TCBCopyRegisters, 194 TCBConfigure, 195 TCBSetPriority, 196 TCBSetIPCBuffer, 197 TCBSetSpace, 198 TCBSuspend, 199 TCBResume, 200 CNodeRevoke, 201 CNodeDelete, 202 CNodeRecycle, 203 CNodeCopy, 204 CNodeMint, 205 CNodeMove, 206 CNodeMutate, 207 CNodeRotate, 208 CNodeSaveCaller, 209 IRQIssueIRQHandler, 210 IRQInterruptControl, 211 IRQAckIRQ, 212 IRQSetIRQHandler, 213 IRQClearIRQHandler, 214 IRQSetMode, 215 DomainSetSet, 216 nInvocationLabels 217}; 218enum arch_invocation_label { 219 ARMPDClean_Data = nInvocationLabels + 0, 220 ARMPDInvalidate_Data = nInvocationLabels + 1, 221 ARMPDCleanInvalidate_Data = nInvocationLabels + 2, 222 ARMPDUnify_Instruction = nInvocationLabels + 3, 223 ARMPageTableMap = nInvocationLabels + 4, 224 ARMPageTableUnmap = nInvocationLabels + 5, 225 ARMPageMap = nInvocationLabels + 6, 226 ARMPageRemap = nInvocationLabels + 7, 227 ARMPageUnmap = nInvocationLabels + 8, 228 ARMPageClean_Data = nInvocationLabels + 9, 229 ARMPageInvalidate_Data = nInvocationLabels + 10, 230 ARMPageCleanInvalidate_Data = nInvocationLabels + 11, 231 ARMPageUnify_Instruction = nInvocationLabels + 12, 232 ARMPageGetAddress = nInvocationLabels + 13, 233 ARMASIDControlMakePool = nInvocationLabels + 14, 234 ARMASIDPoolAssign = nInvocationLabels + 15, 235 nArchInvocationLabels 236}; 237enum { 238 seL4_GlobalsFrame = 0xffffc000, 239}; 240static inline seL4_IPCBuffer *seL4_GetIPCBuffer(void) { 241 return *(seL4_IPCBuffer **)seL4_GlobalsFrame; 242} 243static inline seL4_Word seL4_GetMR(int i) { 244 return seL4_GetIPCBuffer()->msg[i]; 245} 246static inline void seL4_SetMR(int i, seL4_Word mr) { 247 seL4_GetIPCBuffer()->msg[i] = mr; 248} 249static inline void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { 250 register seL4_Word destptr asm("r0") = (seL4_Word)dest; 251 register seL4_Word info asm("r1") = msgInfo.words[0]; 252 /* Load beginning of the message into registers. */ 253 register seL4_Word msg0 asm("r2") = seL4_GetMR(0); 254 register seL4_Word msg1 asm("r3") = seL4_GetMR(1); 255 register seL4_Word msg2 asm("r4") = seL4_GetMR(2); 256 register seL4_Word msg3 asm("r5") = seL4_GetMR(3); 257 /* Perform the system call. */ 258 register seL4_Word scno asm("r7") = seL4_SysSend; 259asm volatile("swi %[swi_num]" 260 : "+r"(destptr), "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3), 261 "+r"(info) 262 : [swi_num] "i"((seL4_SysSend)&0x00ffffff), "r"(scno) 263 : "memory"); 264} 265static inline seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender) { 266 register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; 267 register seL4_MessageInfo_t info asm("r1"); 268 /* Incoming message registers. */ 269 register seL4_Word msg0 asm("r2"); 270 register seL4_Word msg1 asm("r3"); 271 register seL4_Word msg2 asm("r4"); 272 register seL4_Word msg3 asm("r5"); 273 /* Perform the system call. */ 274 register seL4_Word scno asm("r7") = seL4_SysWait; 275asm volatile("swi %[swi_num]" 276 : "=r"(msg0), "=r"(msg1), "=r"(msg2), "=r"(msg3), "=r"(info), 277 "+r"(src_and_badge) 278 : [swi_num] "i"((seL4_SysWait)&0x00ffffff), "r"(scno) 279 : "memory"); 280 /* Write the message back out to memory. */ 281 seL4_SetMR(0, msg0); 282 seL4_SetMR(1, msg1); 283 seL4_SetMR(2, msg2); 284 seL4_SetMR(3, msg3); 285 /* Return back sender and message information. */ 286 if (sender) { 287 *sender = src_and_badge; 288 } 289 return (seL4_MessageInfo_t){.words = {info.words[0]}}; 290} 291typedef unsigned long 292 __type_uint8_t_size_incorrect[(sizeof(uint8_t) == 1) ? 1 : -1]; 293typedef unsigned long 294 __type_uint16_t_size_incorrect[(sizeof(uint16_t) == 2) ? 1 : -1]; 295typedef unsigned long 296 __type_uint32_t_size_incorrect[(sizeof(uint32_t) == 4) ? 1 : -1]; 297typedef unsigned long 298 __type_uint64_t_size_incorrect[(sizeof(uint64_t) == 8) ? 1 : -1]; 299typedef unsigned long __type_int_size_incorrect[(sizeof(int) == 4) ? 1 : -1]; 300typedef unsigned long __type_bool_size_incorrect[(sizeof(_Bool) == 1) ? 1 : -1]; 301typedef unsigned long 302 __type_seL4_Word_size_incorrect[(sizeof(seL4_Word) == 4) ? 1 : -1]; 303typedef unsigned long 304 __type_seL4_CapRights_size_incorrect[(sizeof(seL4_CapRights) == 4) ? 1 305 : -1]; 306typedef unsigned long 307 __type_seL4_CapData_t_size_incorrect[(sizeof(seL4_CapData_t) == 4) ? 1 308 : -1]; 309typedef unsigned long 310 __type_seL4_CPtr_size_incorrect[(sizeof(seL4_CPtr) == 4) ? 1 : -1]; 311typedef unsigned long 312 __type_seL4_CNode_size_incorrect[(sizeof(seL4_CNode) == 4) ? 1 : -1]; 313typedef unsigned long 314 __type_seL4_IRQHandler_size_incorrect[(sizeof(seL4_IRQHandler) == 4) ? 1 315 : -1]; 316typedef unsigned long 317 __type_seL4_IRQControl_size_incorrect[(sizeof(seL4_IRQControl) == 4) ? 1 318 : -1]; 319typedef unsigned long 320 __type_seL4_TCB_size_incorrect[(sizeof(seL4_TCB) == 4) ? 1 : -1]; 321typedef unsigned long 322 __type_seL4_Untyped_size_incorrect[(sizeof(seL4_Untyped) == 4) ? 1 : -1]; 323typedef unsigned long 324 __type_seL4_DomainSet_size_incorrect[(sizeof(seL4_DomainSet) == 4) ? 1 325 : -1]; 326typedef unsigned long __type_seL4_ARM_VMAttributes_size_incorrect 327 [(sizeof(seL4_ARM_VMAttributes) == 4) ? 1 : -1]; 328typedef unsigned long 329 __type_seL4_ARM_Page_size_incorrect[(sizeof(seL4_ARM_Page) == 4) ? 1 : -1]; 330typedef unsigned long __type_seL4_ARM_PageTable_size_incorrect 331 [(sizeof(seL4_ARM_PageTable) == 4) ? 1 : -1]; 332typedef unsigned long __type_seL4_ARM_PageDirectory_size_incorrect 333 [(sizeof(seL4_ARM_PageDirectory) == 4) ? 1 : -1]; 334typedef unsigned long __type_seL4_ARM_ASIDControl_size_incorrect 335 [(sizeof(seL4_ARM_ASIDControl) == 4) ? 1 : -1]; 336typedef unsigned long __type_seL4_ARM_ASIDPool_size_incorrect 337 [(sizeof(seL4_ARM_ASIDPool) == 4) ? 1 : -1]; 338typedef unsigned long __type_seL4_UserContext_size_incorrect 339 [(sizeof(seL4_UserContext) == 68) ? 1 : -1]; 340struct seL4_ARM_Page_GetAddress { 341 int error; 342 seL4_Word paddr; 343}; 344typedef struct seL4_ARM_Page_GetAddress seL4_ARM_Page_GetAddress_t; 345enum { 346 seL4_CapNull = 0, 347 /* null cap */ 348 seL4_CapInitThreadTCB = 1, 349 /* initial thread's TCB cap */ 350 seL4_CapInitThreadCNode = 2, 351 /* initial thread's root CNode cap */ 352 seL4_CapInitThreadVSpace = 3, 353 /* initial thread's VSpace cap */ 354 seL4_CapIRQControl = 4, 355 /* global IRQ controller cap */ 356 seL4_CapASIDControl = 5, 357 /* global ASID controller cap */ 358 seL4_CapInitThreadASIDPool = 6, 359 /* initial thread's ASID pool cap */ 360 seL4_CapIOPort = 7, 361 /* global IO port cap (null cap if not supported) */ 362 seL4_CapIOSpace = 8, 363 /* global IO space cap (null cap if no IOMMU support) */ 364 seL4_CapBootInfoFrame = 9, 365 /* bootinfo frame cap */ 366 seL4_CapInitThreadIPCBuffer = 10, 367 /* initial thread's IPC buffer frame cap */ 368 seL4_CapDomain = 11 369 /* global domain controller cap */ 370}; 371typedef struct { 372 seL4_Word start; 373 /* first CNode slot position OF region */ 374 seL4_Word end; 375 /* first CNode slot position AFTER region */ 376} seL4_SlotRegion; 377typedef struct { 378 seL4_Word basePaddr; 379 /* base physical address of device region */ 380 seL4_Word frameSizeBits; 381 /* size (2^n bytes) of a device-region frame */ 382 seL4_SlotRegion frames; 383 /* device-region frame caps */ 384} seL4_DeviceRegion; 385typedef struct { 386 seL4_Word nodeID; 387 /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */ 388 seL4_Word numNodes; 389 /* number of seL4 nodes (1 if uniprocessor) */ 390 seL4_Word numIOPTLevels; 391 /* number of IOMMU PT levels (0 if no IOMMU support) */ 392 seL4_IPCBuffer *ipcBuffer; 393 /* pointer to initial thread's IPC buffer */ 394 seL4_SlotRegion empty; 395 /* empty slots (null caps) */ 396 seL4_SlotRegion sharedFrames; 397 /* shared-frame caps (shared between seL4 nodes) */ 398 seL4_SlotRegion userImageFrames; 399 /* userland-image frame caps */ 400 seL4_SlotRegion userImagePDs; 401 /* userland-image PD caps */ 402 seL4_SlotRegion userImagePTs; 403 /* userland-image PT caps */ 404 seL4_SlotRegion untyped; 405 /* untyped-object caps (untyped caps) */ 406 seL4_Word untypedPaddrList[167]; 407 /* physical address of each untyped cap */ 408 uint8_t untypedSizeBitsList[167]; 409 /* size (2^n) bytes of each untyped cap */ 410 uint8_t initThreadCNodeSizeBits; 411 /* initial thread's root CNode size (2^n slots) */ 412 seL4_Word numDeviceRegions; 413 /* number of device regions */ 414 seL4_DeviceRegion deviceRegions[199]; 415 /* device regions */ 416 uint32_t initThreadDomain; 417 /* Initial thread's domain ID */ 418} seL4_BootInfo; 419_Noreturn void abort(void); 420typedef struct { int quot, rem; } div_t; 421typedef struct { long quot, rem; } ldiv_t; 422typedef struct { long long quot, rem; } lldiv_t; 423typedef struct __locale_struct *locale_t; 424void *memcpy(void *restrict, const void *restrict, size_t); 425void *memset(void *, int, size_t); 426typedef long time_t; 427typedef long suseconds_t; 428typedef int ssize_t; 429typedef unsigned mode_t; 430typedef unsigned int nlink_t; 431typedef long long off_t; 432typedef unsigned long long ino_t; 433typedef unsigned long long dev_t; 434typedef long blksize_t; 435typedef long long blkcnt_t; 436typedef unsigned long long fsblkcnt_t; 437typedef unsigned long long fsfilcnt_t; 438typedef void *timer_t; 439typedef int clockid_t; 440typedef long clock_t; 441typedef int pid_t; 442typedef unsigned id_t; 443typedef unsigned uid_t; 444typedef unsigned gid_t; 445typedef int key_t; 446typedef unsigned useconds_t; 447typedef struct __pthread *pthread_t; 448typedef int pthread_once_t; 449typedef unsigned pthread_key_t; 450typedef int pthread_spinlock_t; 451typedef struct { unsigned __attr; } pthread_mutexattr_t; 452typedef struct { unsigned __attr; } pthread_condattr_t; 453typedef struct { unsigned __attr; } pthread_barrierattr_t; 454typedef struct { unsigned __attr[2]; } pthread_rwlockattr_t; 455void __builtin_unreachable(void); 456typedef struct { struct list_node *head; } list_t; 457struct list_node { 458 void *data; 459 struct list_node *next; 460}; 461typedef char Buf[((1ul << (12)))]; 462typedef struct dataport_ptr_ { 463 uint32_t id; 464 off_t offset; 465} dataport_ptr_t; 466typedef enum { 467 /* No error occurred. Used to indicate normal operation. */ 468 CE_NO_ERROR = 0, 469 /* During marshalling, the next operation if we were to continue would 470 * exceed the size of the target buffer. Note that continuing in the event 471 * of such an error *will* cause an out-of-bounds memory write. 472 */ 473 CE_BUFFER_LENGTH_EXCEEDED, 474 /* In an RPC communication, the method index indicated by the caller was 475 * out of range for the given interface. That is, the method index was 476 * larger than the number of methods in this interface, or it was 477 * negative. 478 */ 479 CE_INVALID_METHOD_INDEX, 480 /* The payload of an RPC (marshalled parameters) was somehow invalid. This 481 * includes cases where an IPC recipient received a message that was 482 * either 483 * too long or too short for what it was expecting. 484 */ 485 CE_MALFORMED_RPC_PAYLOAD, 486 /* A system call that is never expected to fail in normal operation, did 487 * so. Recovery actions are most likely dependent on what and where the 488 * actual failure was. 489 */ 490 CE_SYSCALL_FAILED, 491 /* Some internal memory/bookkeeping allocation the glue code needed to 492 * perform did not complete successfully. It will be difficult to diagnose 493 * the cause of one of these without looking at the location at which the 494 * error was triggered. 495 */ 496 CE_ALLOCATION_FAILURE, 497} camkes_error_type_t; 498typedef enum { 499 /* Used as a sentinel for a context where an action is invalid. Don't ever 500 * return this from an error handler. 501 */ 502 CEA_INVALID = -1, 503 /* Terminate the currently running piece of glue code by returning. If the 504 * offending code was called from a glue code event loop, this generally 505 * means return to the event loop. If the offending code was called from 506 * user code, this means return to user code where the calling function is 507 * expected to be aware (by some out-of-band communication) that an error 508 * has occurred. 509 */ 510 CEA_DISCARD, 511 /* Ignore the error and continue. This is generally dangerous and not what 512 * you want. 513 */ 514 CEA_IGNORE, 515 /* Exit with failure in the current thread. Note that what 'exit' means 516 * here depends on a number of things including whether the thread has a 517 * cap to itself. 518 */ 519 CEA_ABORT, 520 /* Exit with failure and also try to halt the entire system if possible. 521 * This action implies CEA_ABORT and only differs on a debug kernel where 522 * it is possible to stop the system. If you have no error handlers 523 * installed, this is the default action. 524 */ 525 CEA_HALT, 526} camkes_error_action_t; 527typedef uint32_t sel4bench_counter_t; 528typedef struct camkes_tls_t { 529 seL4_CPtr tcb_cap; 530 unsigned int thread_index; 531} camkes_tls_t; 532static inline camkes_tls_t *__attribute__((__unused__)) camkes_get_tls(void) { 533 /* We store TLS data in the same page as the thread's IPC buffer, but at 534 * the start of the page. 535 */ 536 uintptr_t ipc_buffer = (uintptr_t)seL4_GetIPCBuffer(); 537 /* Normally we would just use MASK here, but the verification C parser 538 * doesn't like the GCC extension used in that macro. The following 539 * assertion could be checked at compile-time, but then it appears in 540 * input 541 * to the verification process that causes other problems. 542 */ 543 (void)0; 544 uintptr_t tls = ipc_buffer & ~(((1ul << (12)) - 1ul)); 545 /* We should have enough room for the TLS data preceding the IPC buffer. */ 546 (void)0; 547 /* We'd better be returning a valid pointer. */ 548 (void)0; 549 return (camkes_tls_t *)tls; 550} 551int RPCFrom__run(void) { 552 /* Nothing to be done. */ 553 return 0; 554} 555static int echo_int_i_from_1; 556static int echo_int_i_from_2; 557static int *get_echo_int_i_from(void) __attribute__((__unused__)); 558static int *get_echo_int_i_from(void) { 559 switch (camkes_get_tls()->thread_index) { 560 case 1: 561 return &echo_int_i_from_1; 562 case 2: 563 return &echo_int_i_from_2; 564 default: 565 (void)0; 566 abort(); 567 } 568} 569static unsigned int echo_int_marshal_inputs_i(unsigned int _camkes_offset_13, 570 int i) { 571 void *_camkes_buffer_base_14 __attribute__((__unused__)) = 572 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 573 /* Construct parameter pointers. We do this here to consolidate where we 574 * are taking the address of local variables. In future, we need to avoid 575 * doing this for verification. 576 */ 577 int *_camkes_ptr_15 = (get_echo_int_i_from()); 578 *_camkes_ptr_15 = i; 579 do { 580 (void)0; 581 if (!(!(_camkes_offset_13 + sizeof(*_camkes_ptr_15) > 582 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 583 for (;;) 584 ; 585 } 586 } while (0); 587 memcpy(_camkes_buffer_base_14 + _camkes_offset_13, _camkes_ptr_15, 588 sizeof(*_camkes_ptr_15)); 589 _camkes_offset_13 += sizeof(*_camkes_ptr_15); 590 return _camkes_offset_13; 591} 592static const uint8_t _camkes_method_index_19 = 0; 593static unsigned int echo_int_marshal_inputs(int i) { 594 unsigned int _camkes_length_20 = 0; 595 void *_camkes_buffer_base_21 __attribute__((__unused__)) = 596 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 597 /* Marshal the method index. */ 598 do { 599 (void)0; 600 if (!(!(_camkes_length_20 + sizeof(_camkes_method_index_19) > 601 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 602 for (;;) 603 ; 604 } 605 } while (0); 606 memcpy(_camkes_buffer_base_21, &_camkes_method_index_19, 607 sizeof(_camkes_method_index_19)); 608 _camkes_length_20 += sizeof(_camkes_method_index_19); 609 /* Marshal the parameters. */ 610 _camkes_length_20 = echo_int_marshal_inputs_i(_camkes_length_20, i); 611 if (_camkes_length_20 == 0xffffffffU) { 612 return 0xffffffffU; 613 } 614 (void)0; 615 return _camkes_length_20; 616} 617static unsigned int 618echo_int_unmarshal_outputs__camkes_ret_fn_22(unsigned int _camkes_size_24, 619 unsigned int _camkes_offset_23, 620 int *_camkes_return_25) { 621 void *_camkes_buffer_base_26 __attribute__((__unused__)) = 622 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 623 /* Unmarshal the return value. */ 624 do { 625 (void)0; 626 if (!(!(_camkes_offset_23 + sizeof(*_camkes_return_25) > 627 _camkes_size_24))) { 628 for (;;) 629 ; 630 } 631 } while (0); 632 memcpy(_camkes_return_25, _camkes_buffer_base_26 + _camkes_offset_23, 633 sizeof(*_camkes_return_25)); 634 _camkes_offset_23 += sizeof(*_camkes_return_25); 635 return _camkes_offset_23; 636} 637static int echo_int_unmarshal_outputs(unsigned int _camkes_size_27, 638 int *_camkes_return_28) { 639 unsigned int _camkes_length_29 __attribute__((__unused__)) = 0; 640 void *_camkes_buffer_base_30 __attribute__((__unused__)) = 641 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 642 _camkes_length_29 = echo_int_unmarshal_outputs__camkes_ret_fn_22( 643 _camkes_size_27, _camkes_length_29, _camkes_return_28); 644 if (_camkes_length_29 == 0xffffffffU) { 645 return -1; 646 } 647 /* Unmarshal the parameters. */ 648 do { 649 (void)0; 650 if (!(!(((_camkes_length_29) + 651 ((_camkes_length_29) % (sizeof(seL4_Word)) == 0 652 ? 0 653 : ((sizeof(seL4_Word)) - 654 ((_camkes_length_29) % (sizeof(seL4_Word)))))) != 655 _camkes_size_27))) { 656 for (;;) 657 ; 658 } 659 } while (0); 660 return 0; 661} 662static int _camkes_ret_tls_var_from_31_1; 663static int _camkes_ret_tls_var_from_31_2; 664static int *get__camkes_ret_tls_var_from_31(void) __attribute__((__unused__)); 665static int *get__camkes_ret_tls_var_from_31(void) { 666 switch (camkes_get_tls()->thread_index) { 667 case 1: 668 return &_camkes_ret_tls_var_from_31_1; 669 case 2: 670 return &_camkes_ret_tls_var_from_31_2; 671 default: 672 (void)0; 673 abort(); 674 } 675} 676int RPCFrom_echo_int(int i) { 677 /* nothing */ 678 ; 679 /* nothing */ 680 ; 681 int _camkes_return_33 __attribute__((__unused__)); 682 int *_camkes_return_ptr_34 = (get__camkes_ret_tls_var_from_31()); 683 unsigned int _camkes_length_35 = echo_int_marshal_inputs(i); 684 if (__builtin_expect(!!(_camkes_length_35 == 0xffffffffU), 0)) { 685 /* Error in marshalling; bail out. */ 686 memset(_camkes_return_ptr_34, 0, sizeof(*_camkes_return_ptr_34)); 687 return *_camkes_return_ptr_34; 688 } 689 /* nothing */ 690 ; 691 /* Call the endpoint */ 692 seL4_MessageInfo_t _camkes_info_36 = seL4_MessageInfo_new( 693 0, 0, 0, ((_camkes_length_35) + 694 ((_camkes_length_35) % (sizeof(seL4_Word)) == 0 695 ? 0 696 : ((sizeof(seL4_Word)) - 697 ((_camkes_length_35) % (sizeof(seL4_Word)))))) / 698 sizeof(seL4_Word)); 699 seL4_Send(6, _camkes_info_36); 700 _camkes_info_36 = seL4_Wait(6, ((void *)0)); 701 /* nothing */ 702 ; 703 /* nothing */ 704 ; 705 /* Unmarshal the response */ 706 unsigned int _camkes_size_37 = 707 seL4_MessageInfo_get_length(_camkes_info_36) * sizeof(seL4_Word); 708 int _camkes_error_38 = 709 echo_int_unmarshal_outputs(_camkes_size_37, _camkes_return_ptr_34); 710 if (__builtin_expect(!!(_camkes_error_38 != 0), 0)) { 711 /* Error in unmarshalling; bail out. */ 712 memset(_camkes_return_ptr_34, 0, sizeof(*_camkes_return_ptr_34)); 713 return *_camkes_return_ptr_34; 714 } 715 /* nothing */ 716 ; 717 return *_camkes_return_ptr_34; 718} 719static int echo_int_1_i_from_1; 720static int echo_int_1_i_from_2; 721static int *get_echo_int_1_i_from(void) __attribute__((__unused__)); 722static int *get_echo_int_1_i_from(void) { 723 switch (camkes_get_tls()->thread_index) { 724 case 1: 725 return &echo_int_1_i_from_1; 726 case 2: 727 return &echo_int_1_i_from_2; 728 default: 729 (void)0; 730 abort(); 731 } 732} 733static unsigned int echo_int_1_j_from_1; 734static unsigned int echo_int_1_j_from_2; 735static unsigned int *get_echo_int_1_j_from(void) __attribute__((__unused__)); 736static unsigned int *get_echo_int_1_j_from(void) { 737 switch (camkes_get_tls()->thread_index) { 738 case 1: 739 return &echo_int_1_j_from_1; 740 case 2: 741 return &echo_int_1_j_from_2; 742 default: 743 (void)0; 744 abort(); 745 } 746} 747static int32_t echo_int_1_k_from_1; 748static int32_t echo_int_1_k_from_2; 749static int32_t *get_echo_int_1_k_from(void) __attribute__((__unused__)); 750static int32_t *get_echo_int_1_k_from(void) { 751 switch (camkes_get_tls()->thread_index) { 752 case 1: 753 return &echo_int_1_k_from_1; 754 case 2: 755 return &echo_int_1_k_from_2; 756 default: 757 (void)0; 758 abort(); 759 } 760} 761static uint32_t echo_int_1_l_from_1; 762static uint32_t echo_int_1_l_from_2; 763static uint32_t *get_echo_int_1_l_from(void) __attribute__((__unused__)); 764static uint32_t *get_echo_int_1_l_from(void) { 765 switch (camkes_get_tls()->thread_index) { 766 case 1: 767 return &echo_int_1_l_from_1; 768 case 2: 769 return &echo_int_1_l_from_2; 770 default: 771 (void)0; 772 abort(); 773 } 774} 775static unsigned int echo_int_1_marshal_inputs_i(unsigned int _camkes_offset_39, 776 int i) { 777 void *_camkes_buffer_base_40 __attribute__((__unused__)) = 778 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 779 /* Construct parameter pointers. We do this here to consolidate where we 780 * are taking the address of local variables. In future, we need to avoid 781 * doing this for verification. 782 */ 783 int *_camkes_ptr_41 = (get_echo_int_1_i_from()); 784 *_camkes_ptr_41 = i; 785 do { 786 (void)0; 787 if (!(!(_camkes_offset_39 + sizeof(*_camkes_ptr_41) > 788 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 789 for (;;) 790 ; 791 } 792 } while (0); 793 memcpy(_camkes_buffer_base_40 + _camkes_offset_39, _camkes_ptr_41, 794 sizeof(*_camkes_ptr_41)); 795 _camkes_offset_39 += sizeof(*_camkes_ptr_41); 796 return _camkes_offset_39; 797} 798static unsigned int echo_int_1_marshal_inputs_j(unsigned int _camkes_offset_45, 799 unsigned int j) { 800 void *_camkes_buffer_base_46 __attribute__((__unused__)) = 801 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 802 /* Construct parameter pointers. We do this here to consolidate where we 803 * are taking the address of local variables. In future, we need to avoid 804 * doing this for verification. 805 */ 806 unsigned int *_camkes_ptr_47 = (get_echo_int_1_j_from()); 807 *_camkes_ptr_47 = j; 808 do { 809 (void)0; 810 if (!(!(_camkes_offset_45 + sizeof(*_camkes_ptr_47) > 811 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 812 for (;;) 813 ; 814 } 815 } while (0); 816 memcpy(_camkes_buffer_base_46 + _camkes_offset_45, _camkes_ptr_47, 817 sizeof(*_camkes_ptr_47)); 818 _camkes_offset_45 += sizeof(*_camkes_ptr_47); 819 return _camkes_offset_45; 820} 821static unsigned int echo_int_1_marshal_inputs_k(unsigned int _camkes_offset_51, 822 int32_t k) { 823 void *_camkes_buffer_base_52 __attribute__((__unused__)) = 824 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 825 /* Construct parameter pointers. We do this here to consolidate where we 826 * are taking the address of local variables. In future, we need to avoid 827 * doing this for verification. 828 */ 829 int32_t *_camkes_ptr_53 = (get_echo_int_1_k_from()); 830 *_camkes_ptr_53 = k; 831 do { 832 (void)0; 833 if (!(!(_camkes_offset_51 + sizeof(*_camkes_ptr_53) > 834 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 835 for (;;) 836 ; 837 } 838 } while (0); 839 memcpy(_camkes_buffer_base_52 + _camkes_offset_51, _camkes_ptr_53, 840 sizeof(*_camkes_ptr_53)); 841 _camkes_offset_51 += sizeof(*_camkes_ptr_53); 842 return _camkes_offset_51; 843} 844static unsigned int echo_int_1_marshal_inputs_l(unsigned int _camkes_offset_57, 845 uint32_t l) { 846 void *_camkes_buffer_base_58 __attribute__((__unused__)) = 847 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 848 /* Construct parameter pointers. We do this here to consolidate where we 849 * are taking the address of local variables. In future, we need to avoid 850 * doing this for verification. 851 */ 852 uint32_t *_camkes_ptr_59 = (get_echo_int_1_l_from()); 853 *_camkes_ptr_59 = l; 854 do { 855 (void)0; 856 if (!(!(_camkes_offset_57 + sizeof(*_camkes_ptr_59) > 857 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 858 for (;;) 859 ; 860 } 861 } while (0); 862 memcpy(_camkes_buffer_base_58 + _camkes_offset_57, _camkes_ptr_59, 863 sizeof(*_camkes_ptr_59)); 864 _camkes_offset_57 += sizeof(*_camkes_ptr_59); 865 return _camkes_offset_57; 866} 867static const uint8_t _camkes_method_index_63 = 1; 868static unsigned int echo_int_1_marshal_inputs(int i, unsigned int j, int32_t k, 869 uint32_t l) { 870 unsigned int _camkes_length_64 = 0; 871 void *_camkes_buffer_base_65 __attribute__((__unused__)) = 872 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 873 /* Marshal the method index. */ 874 do { 875 (void)0; 876 if (!(!(_camkes_length_64 + sizeof(_camkes_method_index_63) > 877 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 878 for (;;) 879 ; 880 } 881 } while (0); 882 memcpy(_camkes_buffer_base_65, &_camkes_method_index_63, 883 sizeof(_camkes_method_index_63)); 884 _camkes_length_64 += sizeof(_camkes_method_index_63); 885 /* Marshal the parameters. */ 886 _camkes_length_64 = echo_int_1_marshal_inputs_i(_camkes_length_64, i); 887 if (_camkes_length_64 == 0xffffffffU) { 888 return 0xffffffffU; 889 } 890 _camkes_length_64 = echo_int_1_marshal_inputs_j(_camkes_length_64, j); 891 if (_camkes_length_64 == 0xffffffffU) { 892 return 0xffffffffU; 893 } 894 _camkes_length_64 = echo_int_1_marshal_inputs_k(_camkes_length_64, k); 895 if (_camkes_length_64 == 0xffffffffU) { 896 return 0xffffffffU; 897 } 898 _camkes_length_64 = echo_int_1_marshal_inputs_l(_camkes_length_64, l); 899 if (_camkes_length_64 == 0xffffffffU) { 900 return 0xffffffffU; 901 } 902 (void)0; 903 return _camkes_length_64; 904} 905static unsigned int 906echo_int_1_unmarshal_outputs__camkes_ret_fn_66(unsigned int _camkes_size_68, 907 unsigned int _camkes_offset_67, 908 int *_camkes_return_69) { 909 void *_camkes_buffer_base_70 __attribute__((__unused__)) = 910 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 911 /* Unmarshal the return value. */ 912 do { 913 (void)0; 914 if (!(!(_camkes_offset_67 + sizeof(*_camkes_return_69) > 915 _camkes_size_68))) { 916 for (;;) 917 ; 918 } 919 } while (0); 920 memcpy(_camkes_return_69, _camkes_buffer_base_70 + _camkes_offset_67, 921 sizeof(*_camkes_return_69)); 922 _camkes_offset_67 += sizeof(*_camkes_return_69); 923 return _camkes_offset_67; 924} 925static int echo_int_1_unmarshal_outputs(unsigned int _camkes_size_71, 926 int *_camkes_return_72) { 927 unsigned int _camkes_length_73 __attribute__((__unused__)) = 0; 928 void *_camkes_buffer_base_74 __attribute__((__unused__)) = 929 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 930 _camkes_length_73 = echo_int_1_unmarshal_outputs__camkes_ret_fn_66( 931 _camkes_size_71, _camkes_length_73, _camkes_return_72); 932 if (_camkes_length_73 == 0xffffffffU) { 933 return -1; 934 } 935 /* Unmarshal the parameters. */ 936 do { 937 (void)0; 938 if (!(!(((_camkes_length_73) + 939 ((_camkes_length_73) % (sizeof(seL4_Word)) == 0 940 ? 0 941 : ((sizeof(seL4_Word)) - 942 ((_camkes_length_73) % (sizeof(seL4_Word)))))) != 943 _camkes_size_71))) { 944 for (;;) 945 ; 946 } 947 } while (0); 948 return 0; 949} 950static int _camkes_ret_tls_var_from_75_1; 951static int _camkes_ret_tls_var_from_75_2; 952static int *get__camkes_ret_tls_var_from_75(void) __attribute__((__unused__)); 953static int *get__camkes_ret_tls_var_from_75(void) { 954 switch (camkes_get_tls()->thread_index) { 955 case 1: 956 return &_camkes_ret_tls_var_from_75_1; 957 case 2: 958 return &_camkes_ret_tls_var_from_75_2; 959 default: 960 (void)0; 961 abort(); 962 } 963} 964int RPCFrom_echo_int_1(int i, unsigned int j, int32_t k, uint32_t l) { 965 /* nothing */ 966 ; 967 /* nothing */ 968 ; 969 int _camkes_return_77 __attribute__((__unused__)); 970 int *_camkes_return_ptr_78 = (get__camkes_ret_tls_var_from_75()); 971 unsigned int _camkes_length_79 = echo_int_1_marshal_inputs(i, j, k, l); 972 if (__builtin_expect(!!(_camkes_length_79 == 0xffffffffU), 0)) { 973 /* Error in marshalling; bail out. */ 974 memset(_camkes_return_ptr_78, 0, sizeof(*_camkes_return_ptr_78)); 975 return *_camkes_return_ptr_78; 976 } 977 /* nothing */ 978 ; 979 /* Call the endpoint */ 980 seL4_MessageInfo_t _camkes_info_80 = seL4_MessageInfo_new( 981 0, 0, 0, ((_camkes_length_79) + 982 ((_camkes_length_79) % (sizeof(seL4_Word)) == 0 983 ? 0 984 : ((sizeof(seL4_Word)) - 985 ((_camkes_length_79) % (sizeof(seL4_Word)))))) / 986 sizeof(seL4_Word)); 987 seL4_Send(6, _camkes_info_80); 988 _camkes_info_80 = seL4_Wait(6, ((void *)0)); 989 /* nothing */ 990 ; 991 /* nothing */ 992 ; 993 /* Unmarshal the response */ 994 unsigned int _camkes_size_81 = 995 seL4_MessageInfo_get_length(_camkes_info_80) * sizeof(seL4_Word); 996 int _camkes_error_82 = 997 echo_int_1_unmarshal_outputs(_camkes_size_81, _camkes_return_ptr_78); 998 if (__builtin_expect(!!(_camkes_error_82 != 0), 0)) { 999 /* Error in unmarshalling; bail out. */ 1000 memset(_camkes_return_ptr_78, 0, sizeof(*_camkes_return_ptr_78)); 1001 return *_camkes_return_ptr_78; 1002 } 1003 /* nothing */ 1004 ; 1005 return *_camkes_return_ptr_78; 1006} 1007static int echo_parameter_pin_from_1; 1008static int echo_parameter_pin_from_2; 1009static int *get_echo_parameter_pin_from(void) __attribute__((__unused__)); 1010static int *get_echo_parameter_pin_from(void) { 1011 switch (camkes_get_tls()->thread_index) { 1012 case 1: 1013 return &echo_parameter_pin_from_1; 1014 case 2: 1015 return &echo_parameter_pin_from_2; 1016 default: 1017 (void)0; 1018 abort(); 1019 } 1020} 1021static unsigned int 1022echo_parameter_marshal_inputs_pin(unsigned int _camkes_offset_83, int pin) { 1023 void *_camkes_buffer_base_84 __attribute__((__unused__)) = 1024 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1025 /* Construct parameter pointers. We do this here to consolidate where we 1026 * are taking the address of local variables. In future, we need to avoid 1027 * doing this for verification. 1028 */ 1029 int *_camkes_ptr_85 = (get_echo_parameter_pin_from()); 1030 *_camkes_ptr_85 = pin; 1031 do { 1032 (void)0; 1033 if (!(!(_camkes_offset_83 + sizeof(*_camkes_ptr_85) > 1034 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1035 for (;;) 1036 ; 1037 } 1038 } while (0); 1039 memcpy(_camkes_buffer_base_84 + _camkes_offset_83, _camkes_ptr_85, 1040 sizeof(*_camkes_ptr_85)); 1041 _camkes_offset_83 += sizeof(*_camkes_ptr_85); 1042 return _camkes_offset_83; 1043} 1044static const uint8_t _camkes_method_index_89 = 2; 1045static unsigned int echo_parameter_marshal_inputs(int pin) { 1046 unsigned int _camkes_length_90 = 0; 1047 void *_camkes_buffer_base_91 __attribute__((__unused__)) = 1048 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1049 /* Marshal the method index. */ 1050 do { 1051 (void)0; 1052 if (!(!(_camkes_length_90 + sizeof(_camkes_method_index_89) > 1053 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1054 for (;;) 1055 ; 1056 } 1057 } while (0); 1058 memcpy(_camkes_buffer_base_91, &_camkes_method_index_89, 1059 sizeof(_camkes_method_index_89)); 1060 _camkes_length_90 += sizeof(_camkes_method_index_89); 1061 /* Marshal the parameters. */ 1062 _camkes_length_90 = echo_parameter_marshal_inputs_pin(_camkes_length_90, pin); 1063 if (_camkes_length_90 == 0xffffffffU) { 1064 return 0xffffffffU; 1065 } 1066 (void)0; 1067 return _camkes_length_90; 1068} 1069static unsigned int echo_parameter_unmarshal_outputs__camkes_ret_fn_92( 1070 unsigned int _camkes_size_94, unsigned int _camkes_offset_93, 1071 int *_camkes_return_95) { 1072 void *_camkes_buffer_base_96 __attribute__((__unused__)) = 1073 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1074 /* Unmarshal the return value. */ 1075 do { 1076 (void)0; 1077 if (!(!(_camkes_offset_93 + sizeof(*_camkes_return_95) > 1078 _camkes_size_94))) { 1079 for (;;) 1080 ; 1081 } 1082 } while (0); 1083 memcpy(_camkes_return_95, _camkes_buffer_base_96 + _camkes_offset_93, 1084 sizeof(*_camkes_return_95)); 1085 _camkes_offset_93 += sizeof(*_camkes_return_95); 1086 return _camkes_offset_93; 1087} 1088static unsigned int echo_parameter_unmarshal_outputs_pout( 1089 unsigned int _camkes_size_97, unsigned int _camkes_offset_98, int *pout) { 1090 void *_camkes_buffer_base_99 __attribute__((__unused__)) = 1091 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1092 do { 1093 (void)0; 1094 if (!(!(_camkes_offset_98 + sizeof(*pout) > _camkes_size_97))) { 1095 for (;;) 1096 ; 1097 } 1098 } while (0); 1099 memcpy(pout, _camkes_buffer_base_99 + _camkes_offset_98, sizeof(*pout)); 1100 _camkes_offset_98 += sizeof(*pout); 1101 return _camkes_offset_98; 1102} 1103static int echo_parameter_unmarshal_outputs(unsigned int _camkes_size_100, 1104 int *_camkes_return_101, 1105 int *pout) { 1106 unsigned int _camkes_length_102 __attribute__((__unused__)) = 0; 1107 void *_camkes_buffer_base_103 __attribute__((__unused__)) = 1108 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1109 _camkes_length_102 = echo_parameter_unmarshal_outputs__camkes_ret_fn_92( 1110 _camkes_size_100, _camkes_length_102, _camkes_return_101); 1111 if (_camkes_length_102 == 0xffffffffU) { 1112 return -1; 1113 } 1114 /* Unmarshal the parameters. */ 1115 _camkes_length_102 = echo_parameter_unmarshal_outputs_pout( 1116 _camkes_size_100, _camkes_length_102, pout); 1117 if (_camkes_length_102 == 0xffffffffU) { 1118 return -1; 1119 } 1120 do { 1121 (void)0; 1122 if (!(!(((_camkes_length_102) + 1123 ((_camkes_length_102) % (sizeof(seL4_Word)) == 0 1124 ? 0 1125 : ((sizeof(seL4_Word)) - 1126 ((_camkes_length_102) % (sizeof(seL4_Word)))))) != 1127 _camkes_size_100))) { 1128 for (;;) 1129 ; 1130 } 1131 } while (0); 1132 return 0; 1133} 1134static int _camkes_ret_tls_var_from_104_1; 1135static int _camkes_ret_tls_var_from_104_2; 1136static int *get__camkes_ret_tls_var_from_104(void) __attribute__((__unused__)); 1137static int *get__camkes_ret_tls_var_from_104(void) { 1138 switch (camkes_get_tls()->thread_index) { 1139 case 1: 1140 return &_camkes_ret_tls_var_from_104_1; 1141 case 2: 1142 return &_camkes_ret_tls_var_from_104_2; 1143 default: 1144 (void)0; 1145 abort(); 1146 } 1147} 1148int RPCFrom_echo_parameter(int pin, int *pout) { 1149 /* nothing */ 1150 ; 1151 /* nothing */ 1152 ; 1153 int _camkes_return_106 __attribute__((__unused__)); 1154 int *_camkes_return_ptr_107 = (get__camkes_ret_tls_var_from_104()); 1155 unsigned int _camkes_length_108 = echo_parameter_marshal_inputs(pin); 1156 if (__builtin_expect(!!(_camkes_length_108 == 0xffffffffU), 0)) { 1157 /* Error in marshalling; bail out. */ 1158 memset(_camkes_return_ptr_107, 0, sizeof(*_camkes_return_ptr_107)); 1159 return *_camkes_return_ptr_107; 1160 } 1161 /* nothing */ 1162 ; 1163 /* Call the endpoint */ 1164 seL4_MessageInfo_t _camkes_info_109 = seL4_MessageInfo_new( 1165 0, 0, 0, ((_camkes_length_108) + 1166 ((_camkes_length_108) % (sizeof(seL4_Word)) == 0 1167 ? 0 1168 : ((sizeof(seL4_Word)) - 1169 ((_camkes_length_108) % (sizeof(seL4_Word)))))) / 1170 sizeof(seL4_Word)); 1171 seL4_Send(6, _camkes_info_109); 1172 _camkes_info_109 = seL4_Wait(6, ((void *)0)); 1173 /* nothing */ 1174 ; 1175 /* nothing */ 1176 ; 1177 /* Unmarshal the response */ 1178 unsigned int _camkes_size_110 = 1179 seL4_MessageInfo_get_length(_camkes_info_109) * sizeof(seL4_Word); 1180 int _camkes_error_111 = echo_parameter_unmarshal_outputs( 1181 _camkes_size_110, _camkes_return_ptr_107, pout); 1182 if (__builtin_expect(!!(_camkes_error_111 != 0), 0)) { 1183 /* Error in unmarshalling; bail out. */ 1184 memset(_camkes_return_ptr_107, 0, sizeof(*_camkes_return_ptr_107)); 1185 return *_camkes_return_ptr_107; 1186 } 1187 /* nothing */ 1188 ; 1189 return *_camkes_return_ptr_107; 1190} 1191static char echo_char_i_from_1; 1192static char echo_char_i_from_2; 1193static char *get_echo_char_i_from(void) __attribute__((__unused__)); 1194static char *get_echo_char_i_from(void) { 1195 switch (camkes_get_tls()->thread_index) { 1196 case 1: 1197 return &echo_char_i_from_1; 1198 case 2: 1199 return &echo_char_i_from_2; 1200 default: 1201 (void)0; 1202 abort(); 1203 } 1204} 1205static unsigned int echo_char_marshal_inputs_i(unsigned int _camkes_offset_112, 1206 char i) { 1207 void *_camkes_buffer_base_113 __attribute__((__unused__)) = 1208 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1209 /* Construct parameter pointers. We do this here to consolidate where we 1210 * are taking the address of local variables. In future, we need to avoid 1211 * doing this for verification. 1212 */ 1213 char *_camkes_ptr_114 = (get_echo_char_i_from()); 1214 *_camkes_ptr_114 = i; 1215 do { 1216 (void)0; 1217 if (!(!(_camkes_offset_112 + sizeof(*_camkes_ptr_114) > 1218 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1219 for (;;) 1220 ; 1221 } 1222 } while (0); 1223 memcpy(_camkes_buffer_base_113 + _camkes_offset_112, _camkes_ptr_114, 1224 sizeof(*_camkes_ptr_114)); 1225 _camkes_offset_112 += sizeof(*_camkes_ptr_114); 1226 return _camkes_offset_112; 1227} 1228static const uint8_t _camkes_method_index_118 = 3; 1229static unsigned int echo_char_marshal_inputs(char i) { 1230 unsigned int _camkes_length_119 = 0; 1231 void *_camkes_buffer_base_120 __attribute__((__unused__)) = 1232 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1233 /* Marshal the method index. */ 1234 do { 1235 (void)0; 1236 if (!(!(_camkes_length_119 + sizeof(_camkes_method_index_118) > 1237 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1238 for (;;) 1239 ; 1240 } 1241 } while (0); 1242 memcpy(_camkes_buffer_base_120, &_camkes_method_index_118, 1243 sizeof(_camkes_method_index_118)); 1244 _camkes_length_119 += sizeof(_camkes_method_index_118); 1245 /* Marshal the parameters. */ 1246 _camkes_length_119 = echo_char_marshal_inputs_i(_camkes_length_119, i); 1247 if (_camkes_length_119 == 0xffffffffU) { 1248 return 0xffffffffU; 1249 } 1250 (void)0; 1251 return _camkes_length_119; 1252} 1253static unsigned int 1254echo_char_unmarshal_outputs__camkes_ret_fn_121(unsigned int _camkes_size_123, 1255 unsigned int _camkes_offset_122, 1256 int *_camkes_return_124) { 1257 void *_camkes_buffer_base_125 __attribute__((__unused__)) = 1258 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1259 /* Unmarshal the return value. */ 1260 do { 1261 (void)0; 1262 if (!(!(_camkes_offset_122 + sizeof(*_camkes_return_124) > 1263 _camkes_size_123))) { 1264 for (;;) 1265 ; 1266 } 1267 } while (0); 1268 memcpy(_camkes_return_124, _camkes_buffer_base_125 + _camkes_offset_122, 1269 sizeof(*_camkes_return_124)); 1270 _camkes_offset_122 += sizeof(*_camkes_return_124); 1271 return _camkes_offset_122; 1272} 1273static int echo_char_unmarshal_outputs(unsigned int _camkes_size_126, 1274 int *_camkes_return_127) { 1275 unsigned int _camkes_length_128 __attribute__((__unused__)) = 0; 1276 void *_camkes_buffer_base_129 __attribute__((__unused__)) = 1277 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1278 _camkes_length_128 = echo_char_unmarshal_outputs__camkes_ret_fn_121( 1279 _camkes_size_126, _camkes_length_128, _camkes_return_127); 1280 if (_camkes_length_128 == 0xffffffffU) { 1281 return -1; 1282 } 1283 /* Unmarshal the parameters. */ 1284 do { 1285 (void)0; 1286 if (!(!(((_camkes_length_128) + 1287 ((_camkes_length_128) % (sizeof(seL4_Word)) == 0 1288 ? 0 1289 : ((sizeof(seL4_Word)) - 1290 ((_camkes_length_128) % (sizeof(seL4_Word)))))) != 1291 _camkes_size_126))) { 1292 for (;;) 1293 ; 1294 } 1295 } while (0); 1296 return 0; 1297} 1298static int _camkes_ret_tls_var_from_130_1; 1299static int _camkes_ret_tls_var_from_130_2; 1300static int *get__camkes_ret_tls_var_from_130(void) __attribute__((__unused__)); 1301static int *get__camkes_ret_tls_var_from_130(void) { 1302 switch (camkes_get_tls()->thread_index) { 1303 case 1: 1304 return &_camkes_ret_tls_var_from_130_1; 1305 case 2: 1306 return &_camkes_ret_tls_var_from_130_2; 1307 default: 1308 (void)0; 1309 abort(); 1310 } 1311} 1312int RPCFrom_echo_char(char i) { 1313 /* nothing */ 1314 ; 1315 /* nothing */ 1316 ; 1317 int _camkes_return_132 __attribute__((__unused__)); 1318 int *_camkes_return_ptr_133 = (get__camkes_ret_tls_var_from_130()); 1319 unsigned int _camkes_length_134 = echo_char_marshal_inputs(i); 1320 if (__builtin_expect(!!(_camkes_length_134 == 0xffffffffU), 0)) { 1321 /* Error in marshalling; bail out. */ 1322 memset(_camkes_return_ptr_133, 0, sizeof(*_camkes_return_ptr_133)); 1323 return *_camkes_return_ptr_133; 1324 } 1325 /* nothing */ 1326 ; 1327 /* Call the endpoint */ 1328 seL4_MessageInfo_t _camkes_info_135 = seL4_MessageInfo_new( 1329 0, 0, 0, ((_camkes_length_134) + 1330 ((_camkes_length_134) % (sizeof(seL4_Word)) == 0 1331 ? 0 1332 : ((sizeof(seL4_Word)) - 1333 ((_camkes_length_134) % (sizeof(seL4_Word)))))) / 1334 sizeof(seL4_Word)); 1335 seL4_Send(6, _camkes_info_135); 1336 _camkes_info_135 = seL4_Wait(6, ((void *)0)); 1337 /* nothing */ 1338 ; 1339 /* nothing */ 1340 ; 1341 /* Unmarshal the response */ 1342 unsigned int _camkes_size_136 = 1343 seL4_MessageInfo_get_length(_camkes_info_135) * sizeof(seL4_Word); 1344 int _camkes_error_137 = 1345 echo_char_unmarshal_outputs(_camkes_size_136, _camkes_return_ptr_133); 1346 if (__builtin_expect(!!(_camkes_error_137 != 0), 0)) { 1347 /* Error in unmarshalling; bail out. */ 1348 memset(_camkes_return_ptr_133, 0, sizeof(*_camkes_return_ptr_133)); 1349 return *_camkes_return_ptr_133; 1350 } 1351 /* nothing */ 1352 ; 1353 return *_camkes_return_ptr_133; 1354} 1355static unsigned int 1356increment_char_marshal_inputs_x(unsigned int _camkes_offset_138, char *x) { 1357 void *_camkes_buffer_base_139 __attribute__((__unused__)) = 1358 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1359 /* Construct parameter pointers. We do this here to consolidate where we 1360 * are taking the address of local variables. In future, we need to avoid 1361 * doing this for verification. 1362 */ 1363 char *_camkes_ptr_140 = x; 1364 do { 1365 (void)0; 1366 if (!(!(_camkes_offset_138 + sizeof(*_camkes_ptr_140) > 1367 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1368 for (;;) 1369 ; 1370 } 1371 } while (0); 1372 memcpy(_camkes_buffer_base_139 + _camkes_offset_138, _camkes_ptr_140, 1373 sizeof(*_camkes_ptr_140)); 1374 _camkes_offset_138 += sizeof(*_camkes_ptr_140); 1375 return _camkes_offset_138; 1376} 1377static const uint8_t _camkes_method_index_144 = 4; 1378static unsigned int increment_char_marshal_inputs(char *x) { 1379 unsigned int _camkes_length_145 = 0; 1380 void *_camkes_buffer_base_146 __attribute__((__unused__)) = 1381 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1382 /* Marshal the method index. */ 1383 do { 1384 (void)0; 1385 if (!(!(_camkes_length_145 + sizeof(_camkes_method_index_144) > 1386 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1387 for (;;) 1388 ; 1389 } 1390 } while (0); 1391 memcpy(_camkes_buffer_base_146, &_camkes_method_index_144, 1392 sizeof(_camkes_method_index_144)); 1393 _camkes_length_145 += sizeof(_camkes_method_index_144); 1394 /* Marshal the parameters. */ 1395 _camkes_length_145 = increment_char_marshal_inputs_x(_camkes_length_145, x); 1396 if (_camkes_length_145 == 0xffffffffU) { 1397 return 0xffffffffU; 1398 } 1399 (void)0; 1400 return _camkes_length_145; 1401} 1402static unsigned int 1403increment_char_unmarshal_outputs_x(unsigned int _camkes_size_148, 1404 unsigned int _camkes_offset_149, char *x) { 1405 void *_camkes_buffer_base_150 __attribute__((__unused__)) = 1406 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1407 do { 1408 (void)0; 1409 if (!(!(_camkes_offset_149 + sizeof(*x) > _camkes_size_148))) { 1410 for (;;) 1411 ; 1412 } 1413 } while (0); 1414 memcpy(x, _camkes_buffer_base_150 + _camkes_offset_149, sizeof(*x)); 1415 _camkes_offset_149 += sizeof(*x); 1416 return _camkes_offset_149; 1417} 1418static int increment_char_unmarshal_outputs(unsigned int _camkes_size_151, 1419 char *x) { 1420 unsigned int _camkes_length_153 __attribute__((__unused__)) = 0; 1421 void *_camkes_buffer_base_154 __attribute__((__unused__)) = 1422 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1423 /* Unmarshal the parameters. */ 1424 _camkes_length_153 = increment_char_unmarshal_outputs_x( 1425 _camkes_size_151, _camkes_length_153, x); 1426 if (_camkes_length_153 == 0xffffffffU) { 1427 return -1; 1428 } 1429 do { 1430 (void)0; 1431 if (!(!(((_camkes_length_153) + 1432 ((_camkes_length_153) % (sizeof(seL4_Word)) == 0 1433 ? 0 1434 : ((sizeof(seL4_Word)) - 1435 ((_camkes_length_153) % (sizeof(seL4_Word)))))) != 1436 _camkes_size_151))) { 1437 for (;;) 1438 ; 1439 } 1440 } while (0); 1441 return 0; 1442} 1443void RPCFrom_increment_char(char *x) { 1444 /* nothing */ 1445 ; 1446 /* nothing */ 1447 ; 1448 unsigned int _camkes_length_159 = increment_char_marshal_inputs(x); 1449 if (__builtin_expect(!!(_camkes_length_159 == 0xffffffffU), 0)) { 1450 /* Error in marshalling; bail out. */ 1451 return; 1452 } 1453 /* nothing */ 1454 ; 1455 /* Call the endpoint */ 1456 seL4_MessageInfo_t _camkes_info_160 = seL4_MessageInfo_new( 1457 0, 0, 0, ((_camkes_length_159) + 1458 ((_camkes_length_159) % (sizeof(seL4_Word)) == 0 1459 ? 0 1460 : ((sizeof(seL4_Word)) - 1461 ((_camkes_length_159) % (sizeof(seL4_Word)))))) / 1462 sizeof(seL4_Word)); 1463 seL4_Send(6, _camkes_info_160); 1464 _camkes_info_160 = seL4_Wait(6, ((void *)0)); 1465 /* nothing */ 1466 ; 1467 /* nothing */ 1468 ; 1469 /* Unmarshal the response */ 1470 unsigned int _camkes_size_161 = 1471 seL4_MessageInfo_get_length(_camkes_info_160) * sizeof(seL4_Word); 1472 int _camkes_error_162 = increment_char_unmarshal_outputs(_camkes_size_161, x); 1473 if (__builtin_expect(!!(_camkes_error_162 != 0), 0)) { 1474 /* Error in unmarshalling; bail out. */ 1475 return; 1476 } 1477 /* nothing */ 1478 ; 1479} 1480static unsigned int 1481increment_parameter_marshal_inputs_x(unsigned int _camkes_offset_163, int *x) { 1482 void *_camkes_buffer_base_164 __attribute__((__unused__)) = 1483 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1484 /* Construct parameter pointers. We do this here to consolidate where we 1485 * are taking the address of local variables. In future, we need to avoid 1486 * doing this for verification. 1487 */ 1488 int *_camkes_ptr_165 = x; 1489 do { 1490 (void)0; 1491 if (!(!(_camkes_offset_163 + sizeof(*_camkes_ptr_165) > 1492 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1493 for (;;) 1494 ; 1495 } 1496 } while (0); 1497 memcpy(_camkes_buffer_base_164 + _camkes_offset_163, _camkes_ptr_165, 1498 sizeof(*_camkes_ptr_165)); 1499 _camkes_offset_163 += sizeof(*_camkes_ptr_165); 1500 return _camkes_offset_163; 1501} 1502static const uint8_t _camkes_method_index_169 = 5; 1503static unsigned int increment_parameter_marshal_inputs(int *x) { 1504 unsigned int _camkes_length_170 = 0; 1505 void *_camkes_buffer_base_171 __attribute__((__unused__)) = 1506 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1507 /* Marshal the method index. */ 1508 do { 1509 (void)0; 1510 if (!(!(_camkes_length_170 + sizeof(_camkes_method_index_169) > 1511 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1512 for (;;) 1513 ; 1514 } 1515 } while (0); 1516 memcpy(_camkes_buffer_base_171, &_camkes_method_index_169, 1517 sizeof(_camkes_method_index_169)); 1518 _camkes_length_170 += sizeof(_camkes_method_index_169); 1519 /* Marshal the parameters. */ 1520 _camkes_length_170 = 1521 increment_parameter_marshal_inputs_x(_camkes_length_170, x); 1522 if (_camkes_length_170 == 0xffffffffU) { 1523 return 0xffffffffU; 1524 } 1525 (void)0; 1526 return _camkes_length_170; 1527} 1528static unsigned int increment_parameter_unmarshal_outputs_x( 1529 unsigned int _camkes_size_173, unsigned int _camkes_offset_174, int *x) { 1530 void *_camkes_buffer_base_175 __attribute__((__unused__)) = 1531 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1532 do { 1533 (void)0; 1534 if (!(!(_camkes_offset_174 + sizeof(*x) > _camkes_size_173))) { 1535 for (;;) 1536 ; 1537 } 1538 } while (0); 1539 memcpy(x, _camkes_buffer_base_175 + _camkes_offset_174, sizeof(*x)); 1540 _camkes_offset_174 += sizeof(*x); 1541 return _camkes_offset_174; 1542} 1543static int increment_parameter_unmarshal_outputs(unsigned int _camkes_size_176, 1544 int *x) { 1545 unsigned int _camkes_length_178 __attribute__((__unused__)) = 0; 1546 void *_camkes_buffer_base_179 __attribute__((__unused__)) = 1547 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1548 /* Unmarshal the parameters. */ 1549 _camkes_length_178 = increment_parameter_unmarshal_outputs_x( 1550 _camkes_size_176, _camkes_length_178, x); 1551 if (_camkes_length_178 == 0xffffffffU) { 1552 return -1; 1553 } 1554 do { 1555 (void)0; 1556 if (!(!(((_camkes_length_178) + 1557 ((_camkes_length_178) % (sizeof(seL4_Word)) == 0 1558 ? 0 1559 : ((sizeof(seL4_Word)) - 1560 ((_camkes_length_178) % (sizeof(seL4_Word)))))) != 1561 _camkes_size_176))) { 1562 for (;;) 1563 ; 1564 } 1565 } while (0); 1566 return 0; 1567} 1568void RPCFrom_increment_parameter(int *x) { 1569 /* nothing */ 1570 ; 1571 /* nothing */ 1572 ; 1573 unsigned int _camkes_length_184 = increment_parameter_marshal_inputs(x); 1574 if (__builtin_expect(!!(_camkes_length_184 == 0xffffffffU), 0)) { 1575 /* Error in marshalling; bail out. */ 1576 return; 1577 } 1578 /* nothing */ 1579 ; 1580 /* Call the endpoint */ 1581 seL4_MessageInfo_t _camkes_info_185 = seL4_MessageInfo_new( 1582 0, 0, 0, ((_camkes_length_184) + 1583 ((_camkes_length_184) % (sizeof(seL4_Word)) == 0 1584 ? 0 1585 : ((sizeof(seL4_Word)) - 1586 ((_camkes_length_184) % (sizeof(seL4_Word)))))) / 1587 sizeof(seL4_Word)); 1588 seL4_Send(6, _camkes_info_185); 1589 _camkes_info_185 = seL4_Wait(6, ((void *)0)); 1590 /* nothing */ 1591 ; 1592 /* nothing */ 1593 ; 1594 /* Unmarshal the response */ 1595 unsigned int _camkes_size_186 = 1596 seL4_MessageInfo_get_length(_camkes_info_185) * sizeof(seL4_Word); 1597 int _camkes_error_187 = 1598 increment_parameter_unmarshal_outputs(_camkes_size_186, x); 1599 if (__builtin_expect(!!(_camkes_error_187 != 0), 0)) { 1600 /* Error in unmarshalling; bail out. */ 1601 return; 1602 } 1603 /* nothing */ 1604 ; 1605} 1606static int echo_int_2_i_from_1; 1607static int echo_int_2_i_from_2; 1608static int *get_echo_int_2_i_from(void) __attribute__((__unused__)); 1609static int *get_echo_int_2_i_from(void) { 1610 switch (camkes_get_tls()->thread_index) { 1611 case 1: 1612 return &echo_int_2_i_from_1; 1613 case 2: 1614 return &echo_int_2_i_from_2; 1615 default: 1616 (void)0; 1617 abort(); 1618 } 1619} 1620static int echo_int_2_j_from_1; 1621static int echo_int_2_j_from_2; 1622static int *get_echo_int_2_j_from(void) __attribute__((__unused__)); 1623static int *get_echo_int_2_j_from(void) { 1624 switch (camkes_get_tls()->thread_index) { 1625 case 1: 1626 return &echo_int_2_j_from_1; 1627 case 2: 1628 return &echo_int_2_j_from_2; 1629 default: 1630 (void)0; 1631 abort(); 1632 } 1633} 1634static unsigned int echo_int_2_marshal_inputs_i(unsigned int _camkes_offset_188, 1635 int i) { 1636 void *_camkes_buffer_base_189 __attribute__((__unused__)) = 1637 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1638 /* Construct parameter pointers. We do this here to consolidate where we 1639 * are taking the address of local variables. In future, we need to avoid 1640 * doing this for verification. 1641 */ 1642 int *_camkes_ptr_190 = (get_echo_int_2_i_from()); 1643 *_camkes_ptr_190 = i; 1644 do { 1645 (void)0; 1646 if (!(!(_camkes_offset_188 + sizeof(*_camkes_ptr_190) > 1647 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1648 for (;;) 1649 ; 1650 } 1651 } while (0); 1652 memcpy(_camkes_buffer_base_189 + _camkes_offset_188, _camkes_ptr_190, 1653 sizeof(*_camkes_ptr_190)); 1654 _camkes_offset_188 += sizeof(*_camkes_ptr_190); 1655 return _camkes_offset_188; 1656} 1657static unsigned int echo_int_2_marshal_inputs_j(unsigned int _camkes_offset_194, 1658 int j) { 1659 void *_camkes_buffer_base_195 __attribute__((__unused__)) = 1660 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1661 /* Construct parameter pointers. We do this here to consolidate where we 1662 * are taking the address of local variables. In future, we need to avoid 1663 * doing this for verification. 1664 */ 1665 int *_camkes_ptr_196 = (get_echo_int_2_j_from()); 1666 *_camkes_ptr_196 = j; 1667 do { 1668 (void)0; 1669 if (!(!(_camkes_offset_194 + sizeof(*_camkes_ptr_196) > 1670 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1671 for (;;) 1672 ; 1673 } 1674 } while (0); 1675 memcpy(_camkes_buffer_base_195 + _camkes_offset_194, _camkes_ptr_196, 1676 sizeof(*_camkes_ptr_196)); 1677 _camkes_offset_194 += sizeof(*_camkes_ptr_196); 1678 return _camkes_offset_194; 1679} 1680static const uint8_t _camkes_method_index_200 = 6; 1681static unsigned int echo_int_2_marshal_inputs(int i, int j) { 1682 unsigned int _camkes_length_201 = 0; 1683 void *_camkes_buffer_base_202 __attribute__((__unused__)) = 1684 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1685 /* Marshal the method index. */ 1686 do { 1687 (void)0; 1688 if (!(!(_camkes_length_201 + sizeof(_camkes_method_index_200) > 1689 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1690 for (;;) 1691 ; 1692 } 1693 } while (0); 1694 memcpy(_camkes_buffer_base_202, &_camkes_method_index_200, 1695 sizeof(_camkes_method_index_200)); 1696 _camkes_length_201 += sizeof(_camkes_method_index_200); 1697 /* Marshal the parameters. */ 1698 _camkes_length_201 = echo_int_2_marshal_inputs_i(_camkes_length_201, i); 1699 if (_camkes_length_201 == 0xffffffffU) { 1700 return 0xffffffffU; 1701 } 1702 _camkes_length_201 = echo_int_2_marshal_inputs_j(_camkes_length_201, j); 1703 if (_camkes_length_201 == 0xffffffffU) { 1704 return 0xffffffffU; 1705 } 1706 (void)0; 1707 return _camkes_length_201; 1708} 1709static unsigned int 1710echo_int_2_unmarshal_outputs__camkes_ret_fn_203(unsigned int _camkes_size_205, 1711 unsigned int _camkes_offset_204, 1712 int *_camkes_return_206) { 1713 void *_camkes_buffer_base_207 __attribute__((__unused__)) = 1714 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1715 /* Unmarshal the return value. */ 1716 do { 1717 (void)0; 1718 if (!(!(_camkes_offset_204 + sizeof(*_camkes_return_206) > 1719 _camkes_size_205))) { 1720 for (;;) 1721 ; 1722 } 1723 } while (0); 1724 memcpy(_camkes_return_206, _camkes_buffer_base_207 + _camkes_offset_204, 1725 sizeof(*_camkes_return_206)); 1726 _camkes_offset_204 += sizeof(*_camkes_return_206); 1727 return _camkes_offset_204; 1728} 1729static int echo_int_2_unmarshal_outputs(unsigned int _camkes_size_208, 1730 int *_camkes_return_209) { 1731 unsigned int _camkes_length_210 __attribute__((__unused__)) = 0; 1732 void *_camkes_buffer_base_211 __attribute__((__unused__)) = 1733 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1734 _camkes_length_210 = echo_int_2_unmarshal_outputs__camkes_ret_fn_203( 1735 _camkes_size_208, _camkes_length_210, _camkes_return_209); 1736 if (_camkes_length_210 == 0xffffffffU) { 1737 return -1; 1738 } 1739 /* Unmarshal the parameters. */ 1740 do { 1741 (void)0; 1742 if (!(!(((_camkes_length_210) + 1743 ((_camkes_length_210) % (sizeof(seL4_Word)) == 0 1744 ? 0 1745 : ((sizeof(seL4_Word)) - 1746 ((_camkes_length_210) % (sizeof(seL4_Word)))))) != 1747 _camkes_size_208))) { 1748 for (;;) 1749 ; 1750 } 1751 } while (0); 1752 return 0; 1753} 1754static int _camkes_ret_tls_var_from_212_1; 1755static int _camkes_ret_tls_var_from_212_2; 1756static int *get__camkes_ret_tls_var_from_212(void) __attribute__((__unused__)); 1757static int *get__camkes_ret_tls_var_from_212(void) { 1758 switch (camkes_get_tls()->thread_index) { 1759 case 1: 1760 return &_camkes_ret_tls_var_from_212_1; 1761 case 2: 1762 return &_camkes_ret_tls_var_from_212_2; 1763 default: 1764 (void)0; 1765 abort(); 1766 } 1767} 1768int RPCFrom_echo_int_2(int i, int j) { 1769 /* nothing */ 1770 ; 1771 /* nothing */ 1772 ; 1773 int _camkes_return_214 __attribute__((__unused__)); 1774 int *_camkes_return_ptr_215 = (get__camkes_ret_tls_var_from_212()); 1775 unsigned int _camkes_length_216 = echo_int_2_marshal_inputs(i, j); 1776 if (__builtin_expect(!!(_camkes_length_216 == 0xffffffffU), 0)) { 1777 /* Error in marshalling; bail out. */ 1778 memset(_camkes_return_ptr_215, 0, sizeof(*_camkes_return_ptr_215)); 1779 return *_camkes_return_ptr_215; 1780 } 1781 /* nothing */ 1782 ; 1783 /* Call the endpoint */ 1784 seL4_MessageInfo_t _camkes_info_217 = seL4_MessageInfo_new( 1785 0, 0, 0, ((_camkes_length_216) + 1786 ((_camkes_length_216) % (sizeof(seL4_Word)) == 0 1787 ? 0 1788 : ((sizeof(seL4_Word)) - 1789 ((_camkes_length_216) % (sizeof(seL4_Word)))))) / 1790 sizeof(seL4_Word)); 1791 seL4_Send(6, _camkes_info_217); 1792 _camkes_info_217 = seL4_Wait(6, ((void *)0)); 1793 /* nothing */ 1794 ; 1795 /* nothing */ 1796 ; 1797 /* Unmarshal the response */ 1798 unsigned int _camkes_size_218 = 1799 seL4_MessageInfo_get_length(_camkes_info_217) * sizeof(seL4_Word); 1800 int _camkes_error_219 = 1801 echo_int_2_unmarshal_outputs(_camkes_size_218, _camkes_return_ptr_215); 1802 if (__builtin_expect(!!(_camkes_error_219 != 0), 0)) { 1803 /* Error in unmarshalling; bail out. */ 1804 memset(_camkes_return_ptr_215, 0, sizeof(*_camkes_return_ptr_215)); 1805 return *_camkes_return_ptr_215; 1806 } 1807 /* nothing */ 1808 ; 1809 return *_camkes_return_ptr_215; 1810} 1811static int echo_int_3_i_from_1; 1812static int echo_int_3_i_from_2; 1813static int *get_echo_int_3_i_from(void) __attribute__((__unused__)); 1814static int *get_echo_int_3_i_from(void) { 1815 switch (camkes_get_tls()->thread_index) { 1816 case 1: 1817 return &echo_int_3_i_from_1; 1818 case 2: 1819 return &echo_int_3_i_from_2; 1820 default: 1821 (void)0; 1822 abort(); 1823 } 1824} 1825static char echo_int_3_j_from_1; 1826static char echo_int_3_j_from_2; 1827static char *get_echo_int_3_j_from(void) __attribute__((__unused__)); 1828static char *get_echo_int_3_j_from(void) { 1829 switch (camkes_get_tls()->thread_index) { 1830 case 1: 1831 return &echo_int_3_j_from_1; 1832 case 2: 1833 return &echo_int_3_j_from_2; 1834 default: 1835 (void)0; 1836 abort(); 1837 } 1838} 1839static unsigned int echo_int_3_marshal_inputs_i(unsigned int _camkes_offset_220, 1840 int i) { 1841 void *_camkes_buffer_base_221 __attribute__((__unused__)) = 1842 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1843 /* Construct parameter pointers. We do this here to consolidate where we 1844 * are taking the address of local variables. In future, we need to avoid 1845 * doing this for verification. 1846 */ 1847 int *_camkes_ptr_222 = (get_echo_int_3_i_from()); 1848 *_camkes_ptr_222 = i; 1849 do { 1850 (void)0; 1851 if (!(!(_camkes_offset_220 + sizeof(*_camkes_ptr_222) > 1852 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1853 for (;;) 1854 ; 1855 } 1856 } while (0); 1857 memcpy(_camkes_buffer_base_221 + _camkes_offset_220, _camkes_ptr_222, 1858 sizeof(*_camkes_ptr_222)); 1859 _camkes_offset_220 += sizeof(*_camkes_ptr_222); 1860 return _camkes_offset_220; 1861} 1862static unsigned int echo_int_3_marshal_inputs_j(unsigned int _camkes_offset_226, 1863 char j) { 1864 void *_camkes_buffer_base_227 __attribute__((__unused__)) = 1865 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1866 /* Construct parameter pointers. We do this here to consolidate where we 1867 * are taking the address of local variables. In future, we need to avoid 1868 * doing this for verification. 1869 */ 1870 char *_camkes_ptr_228 = (get_echo_int_3_j_from()); 1871 *_camkes_ptr_228 = j; 1872 do { 1873 (void)0; 1874 if (!(!(_camkes_offset_226 + sizeof(*_camkes_ptr_228) > 1875 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1876 for (;;) 1877 ; 1878 } 1879 } while (0); 1880 memcpy(_camkes_buffer_base_227 + _camkes_offset_226, _camkes_ptr_228, 1881 sizeof(*_camkes_ptr_228)); 1882 _camkes_offset_226 += sizeof(*_camkes_ptr_228); 1883 return _camkes_offset_226; 1884} 1885static const uint8_t _camkes_method_index_232 = 7; 1886static unsigned int echo_int_3_marshal_inputs(int i, char j) { 1887 unsigned int _camkes_length_233 = 0; 1888 void *_camkes_buffer_base_234 __attribute__((__unused__)) = 1889 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1890 /* Marshal the method index. */ 1891 do { 1892 (void)0; 1893 if (!(!(_camkes_length_233 + sizeof(_camkes_method_index_232) > 1894 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 1895 for (;;) 1896 ; 1897 } 1898 } while (0); 1899 memcpy(_camkes_buffer_base_234, &_camkes_method_index_232, 1900 sizeof(_camkes_method_index_232)); 1901 _camkes_length_233 += sizeof(_camkes_method_index_232); 1902 /* Marshal the parameters. */ 1903 _camkes_length_233 = echo_int_3_marshal_inputs_i(_camkes_length_233, i); 1904 if (_camkes_length_233 == 0xffffffffU) { 1905 return 0xffffffffU; 1906 } 1907 _camkes_length_233 = echo_int_3_marshal_inputs_j(_camkes_length_233, j); 1908 if (_camkes_length_233 == 0xffffffffU) { 1909 return 0xffffffffU; 1910 } 1911 (void)0; 1912 return _camkes_length_233; 1913} 1914static unsigned int 1915echo_int_3_unmarshal_outputs__camkes_ret_fn_235(unsigned int _camkes_size_237, 1916 unsigned int _camkes_offset_236, 1917 int *_camkes_return_238) { 1918 void *_camkes_buffer_base_239 __attribute__((__unused__)) = 1919 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1920 /* Unmarshal the return value. */ 1921 do { 1922 (void)0; 1923 if (!(!(_camkes_offset_236 + sizeof(*_camkes_return_238) > 1924 _camkes_size_237))) { 1925 for (;;) 1926 ; 1927 } 1928 } while (0); 1929 memcpy(_camkes_return_238, _camkes_buffer_base_239 + _camkes_offset_236, 1930 sizeof(*_camkes_return_238)); 1931 _camkes_offset_236 += sizeof(*_camkes_return_238); 1932 return _camkes_offset_236; 1933} 1934static int echo_int_3_unmarshal_outputs(unsigned int _camkes_size_240, 1935 int *_camkes_return_241) { 1936 unsigned int _camkes_length_242 __attribute__((__unused__)) = 0; 1937 void *_camkes_buffer_base_243 __attribute__((__unused__)) = 1938 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 1939 _camkes_length_242 = echo_int_3_unmarshal_outputs__camkes_ret_fn_235( 1940 _camkes_size_240, _camkes_length_242, _camkes_return_241); 1941 if (_camkes_length_242 == 0xffffffffU) { 1942 return -1; 1943 } 1944 /* Unmarshal the parameters. */ 1945 do { 1946 (void)0; 1947 if (!(!(((_camkes_length_242) + 1948 ((_camkes_length_242) % (sizeof(seL4_Word)) == 0 1949 ? 0 1950 : ((sizeof(seL4_Word)) - 1951 ((_camkes_length_242) % (sizeof(seL4_Word)))))) != 1952 _camkes_size_240))) { 1953 for (;;) 1954 ; 1955 } 1956 } while (0); 1957 return 0; 1958} 1959static int _camkes_ret_tls_var_from_244_1; 1960static int _camkes_ret_tls_var_from_244_2; 1961static int *get__camkes_ret_tls_var_from_244(void) __attribute__((__unused__)); 1962static int *get__camkes_ret_tls_var_from_244(void) { 1963 switch (camkes_get_tls()->thread_index) { 1964 case 1: 1965 return &_camkes_ret_tls_var_from_244_1; 1966 case 2: 1967 return &_camkes_ret_tls_var_from_244_2; 1968 default: 1969 (void)0; 1970 abort(); 1971 } 1972} 1973int RPCFrom_echo_int_3(int i, char j) { 1974 /* nothing */ 1975 ; 1976 /* nothing */ 1977 ; 1978 int _camkes_return_246 __attribute__((__unused__)); 1979 int *_camkes_return_ptr_247 = (get__camkes_ret_tls_var_from_244()); 1980 unsigned int _camkes_length_248 = echo_int_3_marshal_inputs(i, j); 1981 if (__builtin_expect(!!(_camkes_length_248 == 0xffffffffU), 0)) { 1982 /* Error in marshalling; bail out. */ 1983 memset(_camkes_return_ptr_247, 0, sizeof(*_camkes_return_ptr_247)); 1984 return *_camkes_return_ptr_247; 1985 } 1986 /* nothing */ 1987 ; 1988 /* Call the endpoint */ 1989 seL4_MessageInfo_t _camkes_info_249 = seL4_MessageInfo_new( 1990 0, 0, 0, ((_camkes_length_248) + 1991 ((_camkes_length_248) % (sizeof(seL4_Word)) == 0 1992 ? 0 1993 : ((sizeof(seL4_Word)) - 1994 ((_camkes_length_248) % (sizeof(seL4_Word)))))) / 1995 sizeof(seL4_Word)); 1996 seL4_Send(6, _camkes_info_249); 1997 _camkes_info_249 = seL4_Wait(6, ((void *)0)); 1998 /* nothing */ 1999 ; 2000 /* nothing */ 2001 ; 2002 /* Unmarshal the response */ 2003 unsigned int _camkes_size_250 = 2004 seL4_MessageInfo_get_length(_camkes_info_249) * sizeof(seL4_Word); 2005 int _camkes_error_251 = 2006 echo_int_3_unmarshal_outputs(_camkes_size_250, _camkes_return_ptr_247); 2007 if (__builtin_expect(!!(_camkes_error_251 != 0), 0)) { 2008 /* Error in unmarshalling; bail out. */ 2009 memset(_camkes_return_ptr_247, 0, sizeof(*_camkes_return_ptr_247)); 2010 return *_camkes_return_ptr_247; 2011 } 2012 /* nothing */ 2013 ; 2014 return *_camkes_return_ptr_247; 2015} 2016static unsigned int 2017increment_64_marshal_inputs_x(unsigned int _camkes_offset_252, uint64_t *x) { 2018 void *_camkes_buffer_base_253 __attribute__((__unused__)) = 2019 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2020 /* Construct parameter pointers. We do this here to consolidate where we 2021 * are taking the address of local variables. In future, we need to avoid 2022 * doing this for verification. 2023 */ 2024 uint64_t *_camkes_ptr_254 = x; 2025 do { 2026 (void)0; 2027 if (!(!(_camkes_offset_252 + sizeof(*_camkes_ptr_254) > 2028 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2029 for (;;) 2030 ; 2031 } 2032 } while (0); 2033 memcpy(_camkes_buffer_base_253 + _camkes_offset_252, _camkes_ptr_254, 2034 sizeof(*_camkes_ptr_254)); 2035 _camkes_offset_252 += sizeof(*_camkes_ptr_254); 2036 return _camkes_offset_252; 2037} 2038static const uint8_t _camkes_method_index_258 = 8; 2039static unsigned int increment_64_marshal_inputs(uint64_t *x) { 2040 unsigned int _camkes_length_259 = 0; 2041 void *_camkes_buffer_base_260 __attribute__((__unused__)) = 2042 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2043 /* Marshal the method index. */ 2044 do { 2045 (void)0; 2046 if (!(!(_camkes_length_259 + sizeof(_camkes_method_index_258) > 2047 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2048 for (;;) 2049 ; 2050 } 2051 } while (0); 2052 memcpy(_camkes_buffer_base_260, &_camkes_method_index_258, 2053 sizeof(_camkes_method_index_258)); 2054 _camkes_length_259 += sizeof(_camkes_method_index_258); 2055 /* Marshal the parameters. */ 2056 _camkes_length_259 = increment_64_marshal_inputs_x(_camkes_length_259, x); 2057 if (_camkes_length_259 == 0xffffffffU) { 2058 return 0xffffffffU; 2059 } 2060 (void)0; 2061 return _camkes_length_259; 2062} 2063static unsigned int 2064increment_64_unmarshal_outputs_x(unsigned int _camkes_size_262, 2065 unsigned int _camkes_offset_263, uint64_t *x) { 2066 void *_camkes_buffer_base_264 __attribute__((__unused__)) = 2067 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2068 do { 2069 (void)0; 2070 if (!(!(_camkes_offset_263 + sizeof(*x) > _camkes_size_262))) { 2071 for (;;) 2072 ; 2073 } 2074 } while (0); 2075 memcpy(x, _camkes_buffer_base_264 + _camkes_offset_263, sizeof(*x)); 2076 _camkes_offset_263 += sizeof(*x); 2077 return _camkes_offset_263; 2078} 2079static int increment_64_unmarshal_outputs(unsigned int _camkes_size_265, 2080 uint64_t *x) { 2081 unsigned int _camkes_length_267 __attribute__((__unused__)) = 0; 2082 void *_camkes_buffer_base_268 __attribute__((__unused__)) = 2083 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2084 /* Unmarshal the parameters. */ 2085 _camkes_length_267 = 2086 increment_64_unmarshal_outputs_x(_camkes_size_265, _camkes_length_267, x); 2087 if (_camkes_length_267 == 0xffffffffU) { 2088 return -1; 2089 } 2090 do { 2091 (void)0; 2092 if (!(!(((_camkes_length_267) + 2093 ((_camkes_length_267) % (sizeof(seL4_Word)) == 0 2094 ? 0 2095 : ((sizeof(seL4_Word)) - 2096 ((_camkes_length_267) % (sizeof(seL4_Word)))))) != 2097 _camkes_size_265))) { 2098 for (;;) 2099 ; 2100 } 2101 } while (0); 2102 return 0; 2103} 2104void RPCFrom_increment_64(uint64_t *x) { 2105 /* nothing */ 2106 ; 2107 /* nothing */ 2108 ; 2109 unsigned int _camkes_length_273 = increment_64_marshal_inputs(x); 2110 if (__builtin_expect(!!(_camkes_length_273 == 0xffffffffU), 0)) { 2111 /* Error in marshalling; bail out. */ 2112 return; 2113 } 2114 /* nothing */ 2115 ; 2116 /* Call the endpoint */ 2117 seL4_MessageInfo_t _camkes_info_274 = seL4_MessageInfo_new( 2118 0, 0, 0, ((_camkes_length_273) + 2119 ((_camkes_length_273) % (sizeof(seL4_Word)) == 0 2120 ? 0 2121 : ((sizeof(seL4_Word)) - 2122 ((_camkes_length_273) % (sizeof(seL4_Word)))))) / 2123 sizeof(seL4_Word)); 2124 seL4_Send(6, _camkes_info_274); 2125 _camkes_info_274 = seL4_Wait(6, ((void *)0)); 2126 /* nothing */ 2127 ; 2128 /* nothing */ 2129 ; 2130 /* Unmarshal the response */ 2131 unsigned int _camkes_size_275 = 2132 seL4_MessageInfo_get_length(_camkes_info_274) * sizeof(seL4_Word); 2133 int _camkes_error_276 = increment_64_unmarshal_outputs(_camkes_size_275, x); 2134 if (__builtin_expect(!!(_camkes_error_276 != 0), 0)) { 2135 /* Error in unmarshalling; bail out. */ 2136 return; 2137 } 2138 /* nothing */ 2139 ; 2140} 2141static int echo_int_4_i_from_1; 2142static int echo_int_4_i_from_2; 2143static int *get_echo_int_4_i_from(void) __attribute__((__unused__)); 2144static int *get_echo_int_4_i_from(void) { 2145 switch (camkes_get_tls()->thread_index) { 2146 case 1: 2147 return &echo_int_4_i_from_1; 2148 case 2: 2149 return &echo_int_4_i_from_2; 2150 default: 2151 (void)0; 2152 abort(); 2153 } 2154} 2155static int64_t echo_int_4_j_from_1; 2156static int64_t echo_int_4_j_from_2; 2157static int64_t *get_echo_int_4_j_from(void) __attribute__((__unused__)); 2158static int64_t *get_echo_int_4_j_from(void) { 2159 switch (camkes_get_tls()->thread_index) { 2160 case 1: 2161 return &echo_int_4_j_from_1; 2162 case 2: 2163 return &echo_int_4_j_from_2; 2164 default: 2165 (void)0; 2166 abort(); 2167 } 2168} 2169static int echo_int_4_k_from_1; 2170static int echo_int_4_k_from_2; 2171static int *get_echo_int_4_k_from(void) __attribute__((__unused__)); 2172static int *get_echo_int_4_k_from(void) { 2173 switch (camkes_get_tls()->thread_index) { 2174 case 1: 2175 return &echo_int_4_k_from_1; 2176 case 2: 2177 return &echo_int_4_k_from_2; 2178 default: 2179 (void)0; 2180 abort(); 2181 } 2182} 2183static int echo_int_4_l_from_1; 2184static int echo_int_4_l_from_2; 2185static int *get_echo_int_4_l_from(void) __attribute__((__unused__)); 2186static int *get_echo_int_4_l_from(void) { 2187 switch (camkes_get_tls()->thread_index) { 2188 case 1: 2189 return &echo_int_4_l_from_1; 2190 case 2: 2191 return &echo_int_4_l_from_2; 2192 default: 2193 (void)0; 2194 abort(); 2195 } 2196} 2197static unsigned int echo_int_4_marshal_inputs_i(unsigned int _camkes_offset_277, 2198 int i) { 2199 void *_camkes_buffer_base_278 __attribute__((__unused__)) = 2200 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2201 /* Construct parameter pointers. We do this here to consolidate where we 2202 * are taking the address of local variables. In future, we need to avoid 2203 * doing this for verification. 2204 */ 2205 int *_camkes_ptr_279 = (get_echo_int_4_i_from()); 2206 *_camkes_ptr_279 = i; 2207 do { 2208 (void)0; 2209 if (!(!(_camkes_offset_277 + sizeof(*_camkes_ptr_279) > 2210 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2211 for (;;) 2212 ; 2213 } 2214 } while (0); 2215 memcpy(_camkes_buffer_base_278 + _camkes_offset_277, _camkes_ptr_279, 2216 sizeof(*_camkes_ptr_279)); 2217 _camkes_offset_277 += sizeof(*_camkes_ptr_279); 2218 return _camkes_offset_277; 2219} 2220static unsigned int echo_int_4_marshal_inputs_j(unsigned int _camkes_offset_283, 2221 int64_t j) { 2222 void *_camkes_buffer_base_284 __attribute__((__unused__)) = 2223 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2224 /* Construct parameter pointers. We do this here to consolidate where we 2225 * are taking the address of local variables. In future, we need to avoid 2226 * doing this for verification. 2227 */ 2228 int64_t *_camkes_ptr_285 = (get_echo_int_4_j_from()); 2229 *_camkes_ptr_285 = j; 2230 do { 2231 (void)0; 2232 if (!(!(_camkes_offset_283 + sizeof(*_camkes_ptr_285) > 2233 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2234 for (;;) 2235 ; 2236 } 2237 } while (0); 2238 memcpy(_camkes_buffer_base_284 + _camkes_offset_283, _camkes_ptr_285, 2239 sizeof(*_camkes_ptr_285)); 2240 _camkes_offset_283 += sizeof(*_camkes_ptr_285); 2241 return _camkes_offset_283; 2242} 2243static unsigned int echo_int_4_marshal_inputs_k(unsigned int _camkes_offset_289, 2244 int k) { 2245 void *_camkes_buffer_base_290 __attribute__((__unused__)) = 2246 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2247 /* Construct parameter pointers. We do this here to consolidate where we 2248 * are taking the address of local variables. In future, we need to avoid 2249 * doing this for verification. 2250 */ 2251 int *_camkes_ptr_291 = (get_echo_int_4_k_from()); 2252 *_camkes_ptr_291 = k; 2253 do { 2254 (void)0; 2255 if (!(!(_camkes_offset_289 + sizeof(*_camkes_ptr_291) > 2256 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2257 for (;;) 2258 ; 2259 } 2260 } while (0); 2261 memcpy(_camkes_buffer_base_290 + _camkes_offset_289, _camkes_ptr_291, 2262 sizeof(*_camkes_ptr_291)); 2263 _camkes_offset_289 += sizeof(*_camkes_ptr_291); 2264 return _camkes_offset_289; 2265} 2266static unsigned int echo_int_4_marshal_inputs_l(unsigned int _camkes_offset_295, 2267 int l) { 2268 void *_camkes_buffer_base_296 __attribute__((__unused__)) = 2269 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2270 /* Construct parameter pointers. We do this here to consolidate where we 2271 * are taking the address of local variables. In future, we need to avoid 2272 * doing this for verification. 2273 */ 2274 int *_camkes_ptr_297 = (get_echo_int_4_l_from()); 2275 *_camkes_ptr_297 = l; 2276 do { 2277 (void)0; 2278 if (!(!(_camkes_offset_295 + sizeof(*_camkes_ptr_297) > 2279 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2280 for (;;) 2281 ; 2282 } 2283 } while (0); 2284 memcpy(_camkes_buffer_base_296 + _camkes_offset_295, _camkes_ptr_297, 2285 sizeof(*_camkes_ptr_297)); 2286 _camkes_offset_295 += sizeof(*_camkes_ptr_297); 2287 return _camkes_offset_295; 2288} 2289static const uint8_t _camkes_method_index_301 = 9; 2290static unsigned int echo_int_4_marshal_inputs(int i, int64_t j, int k, int l) { 2291 unsigned int _camkes_length_302 = 0; 2292 void *_camkes_buffer_base_303 __attribute__((__unused__)) = 2293 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2294 /* Marshal the method index. */ 2295 do { 2296 (void)0; 2297 if (!(!(_camkes_length_302 + sizeof(_camkes_method_index_301) > 2298 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2299 for (;;) 2300 ; 2301 } 2302 } while (0); 2303 memcpy(_camkes_buffer_base_303, &_camkes_method_index_301, 2304 sizeof(_camkes_method_index_301)); 2305 _camkes_length_302 += sizeof(_camkes_method_index_301); 2306 /* Marshal the parameters. */ 2307 _camkes_length_302 = echo_int_4_marshal_inputs_i(_camkes_length_302, i); 2308 if (_camkes_length_302 == 0xffffffffU) { 2309 return 0xffffffffU; 2310 } 2311 _camkes_length_302 = echo_int_4_marshal_inputs_j(_camkes_length_302, j); 2312 if (_camkes_length_302 == 0xffffffffU) { 2313 return 0xffffffffU; 2314 } 2315 _camkes_length_302 = echo_int_4_marshal_inputs_k(_camkes_length_302, k); 2316 if (_camkes_length_302 == 0xffffffffU) { 2317 return 0xffffffffU; 2318 } 2319 _camkes_length_302 = echo_int_4_marshal_inputs_l(_camkes_length_302, l); 2320 if (_camkes_length_302 == 0xffffffffU) { 2321 return 0xffffffffU; 2322 } 2323 (void)0; 2324 return _camkes_length_302; 2325} 2326static unsigned int 2327echo_int_4_unmarshal_outputs__camkes_ret_fn_304(unsigned int _camkes_size_306, 2328 unsigned int _camkes_offset_305, 2329 int *_camkes_return_307) { 2330 void *_camkes_buffer_base_308 __attribute__((__unused__)) = 2331 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2332 /* Unmarshal the return value. */ 2333 do { 2334 (void)0; 2335 if (!(!(_camkes_offset_305 + sizeof(*_camkes_return_307) > 2336 _camkes_size_306))) { 2337 for (;;) 2338 ; 2339 } 2340 } while (0); 2341 memcpy(_camkes_return_307, _camkes_buffer_base_308 + _camkes_offset_305, 2342 sizeof(*_camkes_return_307)); 2343 _camkes_offset_305 += sizeof(*_camkes_return_307); 2344 return _camkes_offset_305; 2345} 2346static int echo_int_4_unmarshal_outputs(unsigned int _camkes_size_309, 2347 int *_camkes_return_310) { 2348 unsigned int _camkes_length_311 __attribute__((__unused__)) = 0; 2349 void *_camkes_buffer_base_312 __attribute__((__unused__)) = 2350 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2351 _camkes_length_311 = echo_int_4_unmarshal_outputs__camkes_ret_fn_304( 2352 _camkes_size_309, _camkes_length_311, _camkes_return_310); 2353 if (_camkes_length_311 == 0xffffffffU) { 2354 return -1; 2355 } 2356 /* Unmarshal the parameters. */ 2357 do { 2358 (void)0; 2359 if (!(!(((_camkes_length_311) + 2360 ((_camkes_length_311) % (sizeof(seL4_Word)) == 0 2361 ? 0 2362 : ((sizeof(seL4_Word)) - 2363 ((_camkes_length_311) % (sizeof(seL4_Word)))))) != 2364 _camkes_size_309))) { 2365 for (;;) 2366 ; 2367 } 2368 } while (0); 2369 return 0; 2370} 2371static int _camkes_ret_tls_var_from_313_1; 2372static int _camkes_ret_tls_var_from_313_2; 2373static int *get__camkes_ret_tls_var_from_313(void) __attribute__((__unused__)); 2374static int *get__camkes_ret_tls_var_from_313(void) { 2375 switch (camkes_get_tls()->thread_index) { 2376 case 1: 2377 return &_camkes_ret_tls_var_from_313_1; 2378 case 2: 2379 return &_camkes_ret_tls_var_from_313_2; 2380 default: 2381 (void)0; 2382 abort(); 2383 } 2384} 2385int RPCFrom_echo_int_4(int i, int64_t j, int k, int l) { 2386 /* nothing */ 2387 ; 2388 /* nothing */ 2389 ; 2390 int _camkes_return_315 __attribute__((__unused__)); 2391 int *_camkes_return_ptr_316 = (get__camkes_ret_tls_var_from_313()); 2392 unsigned int _camkes_length_317 = echo_int_4_marshal_inputs(i, j, k, l); 2393 if (__builtin_expect(!!(_camkes_length_317 == 0xffffffffU), 0)) { 2394 /* Error in marshalling; bail out. */ 2395 memset(_camkes_return_ptr_316, 0, sizeof(*_camkes_return_ptr_316)); 2396 return *_camkes_return_ptr_316; 2397 } 2398 /* nothing */ 2399 ; 2400 /* Call the endpoint */ 2401 seL4_MessageInfo_t _camkes_info_318 = seL4_MessageInfo_new( 2402 0, 0, 0, ((_camkes_length_317) + 2403 ((_camkes_length_317) % (sizeof(seL4_Word)) == 0 2404 ? 0 2405 : ((sizeof(seL4_Word)) - 2406 ((_camkes_length_317) % (sizeof(seL4_Word)))))) / 2407 sizeof(seL4_Word)); 2408 seL4_Send(6, _camkes_info_318); 2409 _camkes_info_318 = seL4_Wait(6, ((void *)0)); 2410 /* nothing */ 2411 ; 2412 /* nothing */ 2413 ; 2414 /* Unmarshal the response */ 2415 unsigned int _camkes_size_319 = 2416 seL4_MessageInfo_get_length(_camkes_info_318) * sizeof(seL4_Word); 2417 int _camkes_error_320 = 2418 echo_int_4_unmarshal_outputs(_camkes_size_319, _camkes_return_ptr_316); 2419 if (__builtin_expect(!!(_camkes_error_320 != 0), 0)) { 2420 /* Error in unmarshalling; bail out. */ 2421 memset(_camkes_return_ptr_316, 0, sizeof(*_camkes_return_ptr_316)); 2422 return *_camkes_return_ptr_316; 2423 } 2424 /* nothing */ 2425 ; 2426 return *_camkes_return_ptr_316; 2427} 2428extern int RPCTo_echo_int(int i); 2429static unsigned int echo_int_unmarshal_inputs_i(unsigned int _camkes_size_322, 2430 unsigned int _camkes_offset_323, 2431 int *i) { 2432 void *_camkes_buffer_base_324 __attribute__((__unused__)) = 2433 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2434 do { 2435 (void)0; 2436 if (!(!(_camkes_offset_323 + sizeof(*i) > _camkes_size_322))) { 2437 for (;;) 2438 ; 2439 } 2440 } while (0); 2441 memcpy(i, _camkes_buffer_base_324 + _camkes_offset_323, sizeof(*i)); 2442 _camkes_offset_323 += sizeof(*i); 2443 return _camkes_offset_323; 2444} 2445static int echo_int_unmarshal_inputs(unsigned int _camkes_size_325, int *i) { 2446 unsigned int _camkes_length_326 __attribute__((__unused__)) = 0; 2447 void *_camkes_buffer_base_327 __attribute__((__unused__)) = 2448 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2449 /* Step over the method index. */ 2450 _camkes_length_326 += sizeof(uint8_t); 2451 /* Unmarshal input parameters. */ 2452 _camkes_length_326 = 2453 echo_int_unmarshal_inputs_i(_camkes_size_325, _camkes_length_326, i); 2454 if (_camkes_length_326 == 0xffffffffU) { 2455 return -1; 2456 } 2457 do { 2458 (void)0; 2459 if (!(!(((_camkes_length_326) + 2460 ((_camkes_length_326) % (sizeof(seL4_Word)) == 0 2461 ? 0 2462 : ((sizeof(seL4_Word)) - 2463 ((_camkes_length_326) % (sizeof(seL4_Word)))))) != 2464 _camkes_size_325))) { 2465 for (;;) 2466 ; 2467 } 2468 } while (0); 2469 return 0; 2470} 2471static unsigned int 2472echo_int_marshal_outputs__camkes_ret_fn_328(unsigned int _camkes_offset_329, 2473 int *_camkes_return_330) { 2474 void *_camkes_buffer_base_331 __attribute__((__unused__)) = 2475 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2476 /* Marshal the return value. */ 2477 do { 2478 (void)0; 2479 if (!(!(_camkes_offset_329 + sizeof(*_camkes_return_330) > 2480 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2481 for (;;) 2482 ; 2483 } 2484 } while (0); 2485 memcpy(_camkes_buffer_base_331 + _camkes_offset_329, _camkes_return_330, 2486 sizeof(*_camkes_return_330)); 2487 _camkes_offset_329 += sizeof(*_camkes_return_330); 2488 return _camkes_offset_329; 2489} 2490static unsigned int echo_int_marshal_outputs(int *_camkes_return_332) { 2491 unsigned int _camkes_length_333 = 0; 2492 _camkes_length_333 = echo_int_marshal_outputs__camkes_ret_fn_328( 2493 _camkes_length_333, _camkes_return_332); 2494 if (_camkes_length_333 == 0xffffffffU) { 2495 return 0xffffffffU; 2496 } 2497 /* Marshal output parameters. */ 2498 (void)0; 2499 return _camkes_length_333; 2500} 2501static int echo_int_ret_to_1; 2502static int echo_int_ret_to_2; 2503static int *get_echo_int_ret_to(void) __attribute__((__unused__)); 2504static int *get_echo_int_ret_to(void) { 2505 switch (camkes_get_tls()->thread_index) { 2506 case 1: 2507 return &echo_int_ret_to_1; 2508 case 2: 2509 return &echo_int_ret_to_2; 2510 default: 2511 (void)0; 2512 abort(); 2513 } 2514} 2515static int echo_int_i_to_1; 2516static int echo_int_i_to_2; 2517static int *get_echo_int_i_to(void) __attribute__((__unused__)); 2518static int *get_echo_int_i_to(void) { 2519 switch (camkes_get_tls()->thread_index) { 2520 case 1: 2521 return &echo_int_i_to_1; 2522 case 2: 2523 return &echo_int_i_to_2; 2524 default: 2525 (void)0; 2526 abort(); 2527 } 2528} 2529extern int RPCTo_echo_int_1(int i, unsigned int j, int32_t k, uint32_t l); 2530static unsigned int 2531echo_int_1_unmarshal_inputs_i(unsigned int _camkes_size_334, 2532 unsigned int _camkes_offset_335, int *i) { 2533 void *_camkes_buffer_base_336 __attribute__((__unused__)) = 2534 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2535 do { 2536 (void)0; 2537 if (!(!(_camkes_offset_335 + sizeof(*i) > _camkes_size_334))) { 2538 for (;;) 2539 ; 2540 } 2541 } while (0); 2542 memcpy(i, _camkes_buffer_base_336 + _camkes_offset_335, sizeof(*i)); 2543 _camkes_offset_335 += sizeof(*i); 2544 return _camkes_offset_335; 2545} 2546static unsigned int 2547echo_int_1_unmarshal_inputs_j(unsigned int _camkes_size_337, 2548 unsigned int _camkes_offset_338, 2549 unsigned int *j) { 2550 void *_camkes_buffer_base_339 __attribute__((__unused__)) = 2551 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2552 do { 2553 (void)0; 2554 if (!(!(_camkes_offset_338 + sizeof(*j) > _camkes_size_337))) { 2555 for (;;) 2556 ; 2557 } 2558 } while (0); 2559 memcpy(j, _camkes_buffer_base_339 + _camkes_offset_338, sizeof(*j)); 2560 _camkes_offset_338 += sizeof(*j); 2561 return _camkes_offset_338; 2562} 2563static unsigned int 2564echo_int_1_unmarshal_inputs_k(unsigned int _camkes_size_340, 2565 unsigned int _camkes_offset_341, int32_t *k) { 2566 void *_camkes_buffer_base_342 __attribute__((__unused__)) = 2567 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2568 do { 2569 (void)0; 2570 if (!(!(_camkes_offset_341 + sizeof(*k) > _camkes_size_340))) { 2571 for (;;) 2572 ; 2573 } 2574 } while (0); 2575 memcpy(k, _camkes_buffer_base_342 + _camkes_offset_341, sizeof(*k)); 2576 _camkes_offset_341 += sizeof(*k); 2577 return _camkes_offset_341; 2578} 2579static unsigned int 2580echo_int_1_unmarshal_inputs_l(unsigned int _camkes_size_343, 2581 unsigned int _camkes_offset_344, uint32_t *l) { 2582 void *_camkes_buffer_base_345 __attribute__((__unused__)) = 2583 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2584 do { 2585 (void)0; 2586 if (!(!(_camkes_offset_344 + sizeof(*l) > _camkes_size_343))) { 2587 for (;;) 2588 ; 2589 } 2590 } while (0); 2591 memcpy(l, _camkes_buffer_base_345 + _camkes_offset_344, sizeof(*l)); 2592 _camkes_offset_344 += sizeof(*l); 2593 return _camkes_offset_344; 2594} 2595static int echo_int_1_unmarshal_inputs(unsigned int _camkes_size_346, int *i, 2596 unsigned int *j, int32_t *k, 2597 uint32_t *l) { 2598 unsigned int _camkes_length_347 __attribute__((__unused__)) = 0; 2599 void *_camkes_buffer_base_348 __attribute__((__unused__)) = 2600 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2601 /* Step over the method index. */ 2602 _camkes_length_347 += sizeof(uint8_t); 2603 /* Unmarshal input parameters. */ 2604 _camkes_length_347 = 2605 echo_int_1_unmarshal_inputs_i(_camkes_size_346, _camkes_length_347, i); 2606 if (_camkes_length_347 == 0xffffffffU) { 2607 return -1; 2608 } 2609 _camkes_length_347 = 2610 echo_int_1_unmarshal_inputs_j(_camkes_size_346, _camkes_length_347, j); 2611 if (_camkes_length_347 == 0xffffffffU) { 2612 return -1; 2613 } 2614 _camkes_length_347 = 2615 echo_int_1_unmarshal_inputs_k(_camkes_size_346, _camkes_length_347, k); 2616 if (_camkes_length_347 == 0xffffffffU) { 2617 return -1; 2618 } 2619 _camkes_length_347 = 2620 echo_int_1_unmarshal_inputs_l(_camkes_size_346, _camkes_length_347, l); 2621 if (_camkes_length_347 == 0xffffffffU) { 2622 return -1; 2623 } 2624 do { 2625 (void)0; 2626 if (!(!(((_camkes_length_347) + 2627 ((_camkes_length_347) % (sizeof(seL4_Word)) == 0 2628 ? 0 2629 : ((sizeof(seL4_Word)) - 2630 ((_camkes_length_347) % (sizeof(seL4_Word)))))) != 2631 _camkes_size_346))) { 2632 for (;;) 2633 ; 2634 } 2635 } while (0); 2636 return 0; 2637} 2638static unsigned int 2639echo_int_1_marshal_outputs__camkes_ret_fn_349(unsigned int _camkes_offset_350, 2640 int *_camkes_return_351) { 2641 void *_camkes_buffer_base_352 __attribute__((__unused__)) = 2642 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2643 /* Marshal the return value. */ 2644 do { 2645 (void)0; 2646 if (!(!(_camkes_offset_350 + sizeof(*_camkes_return_351) > 2647 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2648 for (;;) 2649 ; 2650 } 2651 } while (0); 2652 memcpy(_camkes_buffer_base_352 + _camkes_offset_350, _camkes_return_351, 2653 sizeof(*_camkes_return_351)); 2654 _camkes_offset_350 += sizeof(*_camkes_return_351); 2655 return _camkes_offset_350; 2656} 2657static unsigned int echo_int_1_marshal_outputs(int *_camkes_return_353) { 2658 unsigned int _camkes_length_354 = 0; 2659 _camkes_length_354 = echo_int_1_marshal_outputs__camkes_ret_fn_349( 2660 _camkes_length_354, _camkes_return_353); 2661 if (_camkes_length_354 == 0xffffffffU) { 2662 return 0xffffffffU; 2663 } 2664 /* Marshal output parameters. */ 2665 (void)0; 2666 return _camkes_length_354; 2667} 2668static int echo_int_1_ret_to_1; 2669static int echo_int_1_ret_to_2; 2670static int *get_echo_int_1_ret_to(void) __attribute__((__unused__)); 2671static int *get_echo_int_1_ret_to(void) { 2672 switch (camkes_get_tls()->thread_index) { 2673 case 1: 2674 return &echo_int_1_ret_to_1; 2675 case 2: 2676 return &echo_int_1_ret_to_2; 2677 default: 2678 (void)0; 2679 abort(); 2680 } 2681} 2682static int echo_int_1_i_to_1; 2683static int echo_int_1_i_to_2; 2684static int *get_echo_int_1_i_to(void) __attribute__((__unused__)); 2685static int *get_echo_int_1_i_to(void) { 2686 switch (camkes_get_tls()->thread_index) { 2687 case 1: 2688 return &echo_int_1_i_to_1; 2689 case 2: 2690 return &echo_int_1_i_to_2; 2691 default: 2692 (void)0; 2693 abort(); 2694 } 2695} 2696static unsigned int echo_int_1_j_to_1; 2697static unsigned int echo_int_1_j_to_2; 2698static unsigned int *get_echo_int_1_j_to(void) __attribute__((__unused__)); 2699static unsigned int *get_echo_int_1_j_to(void) { 2700 switch (camkes_get_tls()->thread_index) { 2701 case 1: 2702 return &echo_int_1_j_to_1; 2703 case 2: 2704 return &echo_int_1_j_to_2; 2705 default: 2706 (void)0; 2707 abort(); 2708 } 2709} 2710static int32_t echo_int_1_k_to_1; 2711static int32_t echo_int_1_k_to_2; 2712static int32_t *get_echo_int_1_k_to(void) __attribute__((__unused__)); 2713static int32_t *get_echo_int_1_k_to(void) { 2714 switch (camkes_get_tls()->thread_index) { 2715 case 1: 2716 return &echo_int_1_k_to_1; 2717 case 2: 2718 return &echo_int_1_k_to_2; 2719 default: 2720 (void)0; 2721 abort(); 2722 } 2723} 2724static uint32_t echo_int_1_l_to_1; 2725static uint32_t echo_int_1_l_to_2; 2726static uint32_t *get_echo_int_1_l_to(void) __attribute__((__unused__)); 2727static uint32_t *get_echo_int_1_l_to(void) { 2728 switch (camkes_get_tls()->thread_index) { 2729 case 1: 2730 return &echo_int_1_l_to_1; 2731 case 2: 2732 return &echo_int_1_l_to_2; 2733 default: 2734 (void)0; 2735 abort(); 2736 } 2737} 2738extern int RPCTo_echo_parameter(int pin, int *pout); 2739static unsigned int 2740echo_parameter_unmarshal_inputs_pin(unsigned int _camkes_size_355, 2741 unsigned int _camkes_offset_356, int *pin) { 2742 void *_camkes_buffer_base_357 __attribute__((__unused__)) = 2743 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2744 do { 2745 (void)0; 2746 if (!(!(_camkes_offset_356 + sizeof(*pin) > _camkes_size_355))) { 2747 for (;;) 2748 ; 2749 } 2750 } while (0); 2751 memcpy(pin, _camkes_buffer_base_357 + _camkes_offset_356, sizeof(*pin)); 2752 _camkes_offset_356 += sizeof(*pin); 2753 return _camkes_offset_356; 2754} 2755static int echo_parameter_unmarshal_inputs(unsigned int _camkes_size_358, 2756 int *pin) { 2757 unsigned int _camkes_length_359 __attribute__((__unused__)) = 0; 2758 void *_camkes_buffer_base_360 __attribute__((__unused__)) = 2759 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2760 /* Step over the method index. */ 2761 _camkes_length_359 += sizeof(uint8_t); 2762 /* Unmarshal input parameters. */ 2763 _camkes_length_359 = echo_parameter_unmarshal_inputs_pin( 2764 _camkes_size_358, _camkes_length_359, pin); 2765 if (_camkes_length_359 == 0xffffffffU) { 2766 return -1; 2767 } 2768 do { 2769 (void)0; 2770 if (!(!(((_camkes_length_359) + 2771 ((_camkes_length_359) % (sizeof(seL4_Word)) == 0 2772 ? 0 2773 : ((sizeof(seL4_Word)) - 2774 ((_camkes_length_359) % (sizeof(seL4_Word)))))) != 2775 _camkes_size_358))) { 2776 for (;;) 2777 ; 2778 } 2779 } while (0); 2780 return 0; 2781} 2782static unsigned int echo_parameter_marshal_outputs__camkes_ret_fn_361( 2783 unsigned int _camkes_offset_362, int *_camkes_return_363) { 2784 void *_camkes_buffer_base_364 __attribute__((__unused__)) = 2785 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2786 /* Marshal the return value. */ 2787 do { 2788 (void)0; 2789 if (!(!(_camkes_offset_362 + sizeof(*_camkes_return_363) > 2790 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2791 for (;;) 2792 ; 2793 } 2794 } while (0); 2795 memcpy(_camkes_buffer_base_364 + _camkes_offset_362, _camkes_return_363, 2796 sizeof(*_camkes_return_363)); 2797 _camkes_offset_362 += sizeof(*_camkes_return_363); 2798 return _camkes_offset_362; 2799} 2800static unsigned int 2801echo_parameter_marshal_outputs_pout(unsigned int _camkes_offset_365, 2802 int *pout) { 2803 void *_camkes_buffer_base_366 __attribute__((__unused__)) = 2804 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2805 do { 2806 (void)0; 2807 if (!(!(_camkes_offset_365 + sizeof(*pout) > 2808 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2809 for (;;) 2810 ; 2811 } 2812 } while (0); 2813 memcpy(_camkes_buffer_base_366 + _camkes_offset_365, pout, sizeof(*pout)); 2814 _camkes_offset_365 += sizeof(*pout); 2815 return _camkes_offset_365; 2816} 2817static unsigned int echo_parameter_marshal_outputs(int *_camkes_return_367, 2818 int *pout) { 2819 unsigned int _camkes_length_368 = 0; 2820 _camkes_length_368 = echo_parameter_marshal_outputs__camkes_ret_fn_361( 2821 _camkes_length_368, _camkes_return_367); 2822 if (_camkes_length_368 == 0xffffffffU) { 2823 return 0xffffffffU; 2824 } 2825 /* Marshal output parameters. */ 2826 _camkes_length_368 = 2827 echo_parameter_marshal_outputs_pout(_camkes_length_368, pout); 2828 if (_camkes_length_368 == 0xffffffffU) { 2829 return 0xffffffffU; 2830 } 2831 (void)0; 2832 return _camkes_length_368; 2833} 2834static int echo_parameter_ret_to_1; 2835static int echo_parameter_ret_to_2; 2836static int *get_echo_parameter_ret_to(void) __attribute__((__unused__)); 2837static int *get_echo_parameter_ret_to(void) { 2838 switch (camkes_get_tls()->thread_index) { 2839 case 1: 2840 return &echo_parameter_ret_to_1; 2841 case 2: 2842 return &echo_parameter_ret_to_2; 2843 default: 2844 (void)0; 2845 abort(); 2846 } 2847} 2848static int echo_parameter_pin_to_1; 2849static int echo_parameter_pin_to_2; 2850static int *get_echo_parameter_pin_to(void) __attribute__((__unused__)); 2851static int *get_echo_parameter_pin_to(void) { 2852 switch (camkes_get_tls()->thread_index) { 2853 case 1: 2854 return &echo_parameter_pin_to_1; 2855 case 2: 2856 return &echo_parameter_pin_to_2; 2857 default: 2858 (void)0; 2859 abort(); 2860 } 2861} 2862static int echo_parameter_pout_to_1; 2863static int echo_parameter_pout_to_2; 2864static int *get_echo_parameter_pout_to(void) __attribute__((__unused__)); 2865static int *get_echo_parameter_pout_to(void) { 2866 switch (camkes_get_tls()->thread_index) { 2867 case 1: 2868 return &echo_parameter_pout_to_1; 2869 case 2: 2870 return &echo_parameter_pout_to_2; 2871 default: 2872 (void)0; 2873 abort(); 2874 } 2875} 2876extern int RPCTo_echo_char(char i); 2877static unsigned int 2878echo_char_unmarshal_inputs_i(unsigned int _camkes_size_369, 2879 unsigned int _camkes_offset_370, char *i) { 2880 void *_camkes_buffer_base_371 __attribute__((__unused__)) = 2881 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2882 do { 2883 (void)0; 2884 if (!(!(_camkes_offset_370 + sizeof(*i) > _camkes_size_369))) { 2885 for (;;) 2886 ; 2887 } 2888 } while (0); 2889 memcpy(i, _camkes_buffer_base_371 + _camkes_offset_370, sizeof(*i)); 2890 _camkes_offset_370 += sizeof(*i); 2891 return _camkes_offset_370; 2892} 2893static int echo_char_unmarshal_inputs(unsigned int _camkes_size_372, char *i) { 2894 unsigned int _camkes_length_373 __attribute__((__unused__)) = 0; 2895 void *_camkes_buffer_base_374 __attribute__((__unused__)) = 2896 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2897 /* Step over the method index. */ 2898 _camkes_length_373 += sizeof(uint8_t); 2899 /* Unmarshal input parameters. */ 2900 _camkes_length_373 = 2901 echo_char_unmarshal_inputs_i(_camkes_size_372, _camkes_length_373, i); 2902 if (_camkes_length_373 == 0xffffffffU) { 2903 return -1; 2904 } 2905 do { 2906 (void)0; 2907 if (!(!(((_camkes_length_373) + 2908 ((_camkes_length_373) % (sizeof(seL4_Word)) == 0 2909 ? 0 2910 : ((sizeof(seL4_Word)) - 2911 ((_camkes_length_373) % (sizeof(seL4_Word)))))) != 2912 _camkes_size_372))) { 2913 for (;;) 2914 ; 2915 } 2916 } while (0); 2917 return 0; 2918} 2919static unsigned int 2920echo_char_marshal_outputs__camkes_ret_fn_375(unsigned int _camkes_offset_376, 2921 int *_camkes_return_377) { 2922 void *_camkes_buffer_base_378 __attribute__((__unused__)) = 2923 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2924 /* Marshal the return value. */ 2925 do { 2926 (void)0; 2927 if (!(!(_camkes_offset_376 + sizeof(*_camkes_return_377) > 2928 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 2929 for (;;) 2930 ; 2931 } 2932 } while (0); 2933 memcpy(_camkes_buffer_base_378 + _camkes_offset_376, _camkes_return_377, 2934 sizeof(*_camkes_return_377)); 2935 _camkes_offset_376 += sizeof(*_camkes_return_377); 2936 return _camkes_offset_376; 2937} 2938static unsigned int echo_char_marshal_outputs(int *_camkes_return_379) { 2939 unsigned int _camkes_length_380 = 0; 2940 _camkes_length_380 = echo_char_marshal_outputs__camkes_ret_fn_375( 2941 _camkes_length_380, _camkes_return_379); 2942 if (_camkes_length_380 == 0xffffffffU) { 2943 return 0xffffffffU; 2944 } 2945 /* Marshal output parameters. */ 2946 (void)0; 2947 return _camkes_length_380; 2948} 2949static int echo_char_ret_to_1; 2950static int echo_char_ret_to_2; 2951static int *get_echo_char_ret_to(void) __attribute__((__unused__)); 2952static int *get_echo_char_ret_to(void) { 2953 switch (camkes_get_tls()->thread_index) { 2954 case 1: 2955 return &echo_char_ret_to_1; 2956 case 2: 2957 return &echo_char_ret_to_2; 2958 default: 2959 (void)0; 2960 abort(); 2961 } 2962} 2963static char echo_char_i_to_1; 2964static char echo_char_i_to_2; 2965static char *get_echo_char_i_to(void) __attribute__((__unused__)); 2966static char *get_echo_char_i_to(void) { 2967 switch (camkes_get_tls()->thread_index) { 2968 case 1: 2969 return &echo_char_i_to_1; 2970 case 2: 2971 return &echo_char_i_to_2; 2972 default: 2973 (void)0; 2974 abort(); 2975 } 2976} 2977extern void RPCTo_increment_char(char *x); 2978static unsigned int 2979increment_char_unmarshal_inputs_x(unsigned int _camkes_size_381, 2980 unsigned int _camkes_offset_382, char *x) { 2981 void *_camkes_buffer_base_383 __attribute__((__unused__)) = 2982 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2983 do { 2984 (void)0; 2985 if (!(!(_camkes_offset_382 + sizeof(*x) > _camkes_size_381))) { 2986 for (;;) 2987 ; 2988 } 2989 } while (0); 2990 memcpy(x, _camkes_buffer_base_383 + _camkes_offset_382, sizeof(*x)); 2991 _camkes_offset_382 += sizeof(*x); 2992 return _camkes_offset_382; 2993} 2994static int increment_char_unmarshal_inputs(unsigned int _camkes_size_384, 2995 char *x) { 2996 unsigned int _camkes_length_385 __attribute__((__unused__)) = 0; 2997 void *_camkes_buffer_base_386 __attribute__((__unused__)) = 2998 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 2999 /* Step over the method index. */ 3000 _camkes_length_385 += sizeof(uint8_t); 3001 /* Unmarshal input parameters. */ 3002 _camkes_length_385 = increment_char_unmarshal_inputs_x(_camkes_size_384, 3003 _camkes_length_385, x); 3004 if (_camkes_length_385 == 0xffffffffU) { 3005 return -1; 3006 } 3007 do { 3008 (void)0; 3009 if (!(!(((_camkes_length_385) + 3010 ((_camkes_length_385) % (sizeof(seL4_Word)) == 0 3011 ? 0 3012 : ((sizeof(seL4_Word)) - 3013 ((_camkes_length_385) % (sizeof(seL4_Word)))))) != 3014 _camkes_size_384))) { 3015 for (;;) 3016 ; 3017 } 3018 } while (0); 3019 return 0; 3020} 3021static unsigned int 3022increment_char_marshal_outputs_x(unsigned int _camkes_offset_388, char *x) { 3023 void *_camkes_buffer_base_389 __attribute__((__unused__)) = 3024 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3025 do { 3026 (void)0; 3027 if (!(!(_camkes_offset_388 + sizeof(*x) > 3028 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3029 for (;;) 3030 ; 3031 } 3032 } while (0); 3033 memcpy(_camkes_buffer_base_389 + _camkes_offset_388, x, sizeof(*x)); 3034 _camkes_offset_388 += sizeof(*x); 3035 return _camkes_offset_388; 3036} 3037static unsigned int increment_char_marshal_outputs(char *x) { 3038 unsigned int _camkes_length_391 = 0; 3039 /* Marshal output parameters. */ 3040 _camkes_length_391 = increment_char_marshal_outputs_x(_camkes_length_391, x); 3041 if (_camkes_length_391 == 0xffffffffU) { 3042 return 0xffffffffU; 3043 } 3044 (void)0; 3045 return _camkes_length_391; 3046} 3047static char increment_char_x_to_1; 3048static char increment_char_x_to_2; 3049static char *get_increment_char_x_to(void) __attribute__((__unused__)); 3050static char *get_increment_char_x_to(void) { 3051 switch (camkes_get_tls()->thread_index) { 3052 case 1: 3053 return &increment_char_x_to_1; 3054 case 2: 3055 return &increment_char_x_to_2; 3056 default: 3057 (void)0; 3058 abort(); 3059 } 3060} 3061extern void RPCTo_increment_parameter(int *x); 3062static unsigned int increment_parameter_unmarshal_inputs_x( 3063 unsigned int _camkes_size_392, unsigned int _camkes_offset_393, int *x) { 3064 void *_camkes_buffer_base_394 __attribute__((__unused__)) = 3065 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3066 do { 3067 (void)0; 3068 if (!(!(_camkes_offset_393 + sizeof(*x) > _camkes_size_392))) { 3069 for (;;) 3070 ; 3071 } 3072 } while (0); 3073 memcpy(x, _camkes_buffer_base_394 + _camkes_offset_393, sizeof(*x)); 3074 _camkes_offset_393 += sizeof(*x); 3075 return _camkes_offset_393; 3076} 3077static int increment_parameter_unmarshal_inputs(unsigned int _camkes_size_395, 3078 int *x) { 3079 unsigned int _camkes_length_396 __attribute__((__unused__)) = 0; 3080 void *_camkes_buffer_base_397 __attribute__((__unused__)) = 3081 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3082 /* Step over the method index. */ 3083 _camkes_length_396 += sizeof(uint8_t); 3084 /* Unmarshal input parameters. */ 3085 _camkes_length_396 = increment_parameter_unmarshal_inputs_x( 3086 _camkes_size_395, _camkes_length_396, x); 3087 if (_camkes_length_396 == 0xffffffffU) { 3088 return -1; 3089 } 3090 do { 3091 (void)0; 3092 if (!(!(((_camkes_length_396) + 3093 ((_camkes_length_396) % (sizeof(seL4_Word)) == 0 3094 ? 0 3095 : ((sizeof(seL4_Word)) - 3096 ((_camkes_length_396) % (sizeof(seL4_Word)))))) != 3097 _camkes_size_395))) { 3098 for (;;) 3099 ; 3100 } 3101 } while (0); 3102 return 0; 3103} 3104static unsigned int 3105increment_parameter_marshal_outputs_x(unsigned int _camkes_offset_399, int *x) { 3106 void *_camkes_buffer_base_400 __attribute__((__unused__)) = 3107 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3108 do { 3109 (void)0; 3110 if (!(!(_camkes_offset_399 + sizeof(*x) > 3111 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3112 for (;;) 3113 ; 3114 } 3115 } while (0); 3116 memcpy(_camkes_buffer_base_400 + _camkes_offset_399, x, sizeof(*x)); 3117 _camkes_offset_399 += sizeof(*x); 3118 return _camkes_offset_399; 3119} 3120static unsigned int increment_parameter_marshal_outputs(int *x) { 3121 unsigned int _camkes_length_402 = 0; 3122 /* Marshal output parameters. */ 3123 _camkes_length_402 = 3124 increment_parameter_marshal_outputs_x(_camkes_length_402, x); 3125 if (_camkes_length_402 == 0xffffffffU) { 3126 return 0xffffffffU; 3127 } 3128 (void)0; 3129 return _camkes_length_402; 3130} 3131static int increment_parameter_x_to_1; 3132static int increment_parameter_x_to_2; 3133static int *get_increment_parameter_x_to(void) __attribute__((__unused__)); 3134static int *get_increment_parameter_x_to(void) { 3135 switch (camkes_get_tls()->thread_index) { 3136 case 1: 3137 return &increment_parameter_x_to_1; 3138 case 2: 3139 return &increment_parameter_x_to_2; 3140 default: 3141 (void)0; 3142 abort(); 3143 } 3144} 3145extern int RPCTo_echo_int_2(int i, int j); 3146static unsigned int 3147echo_int_2_unmarshal_inputs_i(unsigned int _camkes_size_403, 3148 unsigned int _camkes_offset_404, int *i) { 3149 void *_camkes_buffer_base_405 __attribute__((__unused__)) = 3150 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3151 do { 3152 (void)0; 3153 if (!(!(_camkes_offset_404 + sizeof(*i) > _camkes_size_403))) { 3154 for (;;) 3155 ; 3156 } 3157 } while (0); 3158 memcpy(i, _camkes_buffer_base_405 + _camkes_offset_404, sizeof(*i)); 3159 _camkes_offset_404 += sizeof(*i); 3160 return _camkes_offset_404; 3161} 3162static unsigned int 3163echo_int_2_unmarshal_inputs_j(unsigned int _camkes_size_406, 3164 unsigned int _camkes_offset_407, int *j) { 3165 void *_camkes_buffer_base_408 __attribute__((__unused__)) = 3166 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3167 do { 3168 (void)0; 3169 if (!(!(_camkes_offset_407 + sizeof(*j) > _camkes_size_406))) { 3170 for (;;) 3171 ; 3172 } 3173 } while (0); 3174 memcpy(j, _camkes_buffer_base_408 + _camkes_offset_407, sizeof(*j)); 3175 _camkes_offset_407 += sizeof(*j); 3176 return _camkes_offset_407; 3177} 3178static int echo_int_2_unmarshal_inputs(unsigned int _camkes_size_409, int *i, 3179 int *j) { 3180 unsigned int _camkes_length_410 __attribute__((__unused__)) = 0; 3181 void *_camkes_buffer_base_411 __attribute__((__unused__)) = 3182 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3183 /* Step over the method index. */ 3184 _camkes_length_410 += sizeof(uint8_t); 3185 /* Unmarshal input parameters. */ 3186 _camkes_length_410 = 3187 echo_int_2_unmarshal_inputs_i(_camkes_size_409, _camkes_length_410, i); 3188 if (_camkes_length_410 == 0xffffffffU) { 3189 return -1; 3190 } 3191 _camkes_length_410 = 3192 echo_int_2_unmarshal_inputs_j(_camkes_size_409, _camkes_length_410, j); 3193 if (_camkes_length_410 == 0xffffffffU) { 3194 return -1; 3195 } 3196 do { 3197 (void)0; 3198 if (!(!(((_camkes_length_410) + 3199 ((_camkes_length_410) % (sizeof(seL4_Word)) == 0 3200 ? 0 3201 : ((sizeof(seL4_Word)) - 3202 ((_camkes_length_410) % (sizeof(seL4_Word)))))) != 3203 _camkes_size_409))) { 3204 for (;;) 3205 ; 3206 } 3207 } while (0); 3208 return 0; 3209} 3210static unsigned int 3211echo_int_2_marshal_outputs__camkes_ret_fn_412(unsigned int _camkes_offset_413, 3212 int *_camkes_return_414) { 3213 void *_camkes_buffer_base_415 __attribute__((__unused__)) = 3214 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3215 /* Marshal the return value. */ 3216 do { 3217 (void)0; 3218 if (!(!(_camkes_offset_413 + sizeof(*_camkes_return_414) > 3219 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3220 for (;;) 3221 ; 3222 } 3223 } while (0); 3224 memcpy(_camkes_buffer_base_415 + _camkes_offset_413, _camkes_return_414, 3225 sizeof(*_camkes_return_414)); 3226 _camkes_offset_413 += sizeof(*_camkes_return_414); 3227 return _camkes_offset_413; 3228} 3229static unsigned int echo_int_2_marshal_outputs(int *_camkes_return_416) { 3230 unsigned int _camkes_length_417 = 0; 3231 _camkes_length_417 = echo_int_2_marshal_outputs__camkes_ret_fn_412( 3232 _camkes_length_417, _camkes_return_416); 3233 if (_camkes_length_417 == 0xffffffffU) { 3234 return 0xffffffffU; 3235 } 3236 /* Marshal output parameters. */ 3237 (void)0; 3238 return _camkes_length_417; 3239} 3240static int echo_int_2_ret_to_1; 3241static int echo_int_2_ret_to_2; 3242static int *get_echo_int_2_ret_to(void) __attribute__((__unused__)); 3243static int *get_echo_int_2_ret_to(void) { 3244 switch (camkes_get_tls()->thread_index) { 3245 case 1: 3246 return &echo_int_2_ret_to_1; 3247 case 2: 3248 return &echo_int_2_ret_to_2; 3249 default: 3250 (void)0; 3251 abort(); 3252 } 3253} 3254static int echo_int_2_i_to_1; 3255static int echo_int_2_i_to_2; 3256static int *get_echo_int_2_i_to(void) __attribute__((__unused__)); 3257static int *get_echo_int_2_i_to(void) { 3258 switch (camkes_get_tls()->thread_index) { 3259 case 1: 3260 return &echo_int_2_i_to_1; 3261 case 2: 3262 return &echo_int_2_i_to_2; 3263 default: 3264 (void)0; 3265 abort(); 3266 } 3267} 3268static int echo_int_2_j_to_1; 3269static int echo_int_2_j_to_2; 3270static int *get_echo_int_2_j_to(void) __attribute__((__unused__)); 3271static int *get_echo_int_2_j_to(void) { 3272 switch (camkes_get_tls()->thread_index) { 3273 case 1: 3274 return &echo_int_2_j_to_1; 3275 case 2: 3276 return &echo_int_2_j_to_2; 3277 default: 3278 (void)0; 3279 abort(); 3280 } 3281} 3282extern int RPCTo_echo_int_3(int i, char j); 3283static unsigned int 3284echo_int_3_unmarshal_inputs_i(unsigned int _camkes_size_418, 3285 unsigned int _camkes_offset_419, int *i) { 3286 void *_camkes_buffer_base_420 __attribute__((__unused__)) = 3287 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3288 do { 3289 (void)0; 3290 if (!(!(_camkes_offset_419 + sizeof(*i) > _camkes_size_418))) { 3291 for (;;) 3292 ; 3293 } 3294 } while (0); 3295 memcpy(i, _camkes_buffer_base_420 + _camkes_offset_419, sizeof(*i)); 3296 _camkes_offset_419 += sizeof(*i); 3297 return _camkes_offset_419; 3298} 3299static unsigned int 3300echo_int_3_unmarshal_inputs_j(unsigned int _camkes_size_421, 3301 unsigned int _camkes_offset_422, char *j) { 3302 void *_camkes_buffer_base_423 __attribute__((__unused__)) = 3303 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3304 do { 3305 (void)0; 3306 if (!(!(_camkes_offset_422 + sizeof(*j) > _camkes_size_421))) { 3307 for (;;) 3308 ; 3309 } 3310 } while (0); 3311 memcpy(j, _camkes_buffer_base_423 + _camkes_offset_422, sizeof(*j)); 3312 _camkes_offset_422 += sizeof(*j); 3313 return _camkes_offset_422; 3314} 3315static int echo_int_3_unmarshal_inputs(unsigned int _camkes_size_424, int *i, 3316 char *j) { 3317 unsigned int _camkes_length_425 __attribute__((__unused__)) = 0; 3318 void *_camkes_buffer_base_426 __attribute__((__unused__)) = 3319 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3320 /* Step over the method index. */ 3321 _camkes_length_425 += sizeof(uint8_t); 3322 /* Unmarshal input parameters. */ 3323 _camkes_length_425 = 3324 echo_int_3_unmarshal_inputs_i(_camkes_size_424, _camkes_length_425, i); 3325 if (_camkes_length_425 == 0xffffffffU) { 3326 return -1; 3327 } 3328 _camkes_length_425 = 3329 echo_int_3_unmarshal_inputs_j(_camkes_size_424, _camkes_length_425, j); 3330 if (_camkes_length_425 == 0xffffffffU) { 3331 return -1; 3332 } 3333 do { 3334 (void)0; 3335 if (!(!(((_camkes_length_425) + 3336 ((_camkes_length_425) % (sizeof(seL4_Word)) == 0 3337 ? 0 3338 : ((sizeof(seL4_Word)) - 3339 ((_camkes_length_425) % (sizeof(seL4_Word)))))) != 3340 _camkes_size_424))) { 3341 for (;;) 3342 ; 3343 } 3344 } while (0); 3345 return 0; 3346} 3347static unsigned int 3348echo_int_3_marshal_outputs__camkes_ret_fn_427(unsigned int _camkes_offset_428, 3349 int *_camkes_return_429) { 3350 void *_camkes_buffer_base_430 __attribute__((__unused__)) = 3351 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3352 /* Marshal the return value. */ 3353 do { 3354 (void)0; 3355 if (!(!(_camkes_offset_428 + sizeof(*_camkes_return_429) > 3356 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3357 for (;;) 3358 ; 3359 } 3360 } while (0); 3361 memcpy(_camkes_buffer_base_430 + _camkes_offset_428, _camkes_return_429, 3362 sizeof(*_camkes_return_429)); 3363 _camkes_offset_428 += sizeof(*_camkes_return_429); 3364 return _camkes_offset_428; 3365} 3366static unsigned int echo_int_3_marshal_outputs(int *_camkes_return_431) { 3367 unsigned int _camkes_length_432 = 0; 3368 _camkes_length_432 = echo_int_3_marshal_outputs__camkes_ret_fn_427( 3369 _camkes_length_432, _camkes_return_431); 3370 if (_camkes_length_432 == 0xffffffffU) { 3371 return 0xffffffffU; 3372 } 3373 /* Marshal output parameters. */ 3374 (void)0; 3375 return _camkes_length_432; 3376} 3377static int echo_int_3_ret_to_1; 3378static int echo_int_3_ret_to_2; 3379static int *get_echo_int_3_ret_to(void) __attribute__((__unused__)); 3380static int *get_echo_int_3_ret_to(void) { 3381 switch (camkes_get_tls()->thread_index) { 3382 case 1: 3383 return &echo_int_3_ret_to_1; 3384 case 2: 3385 return &echo_int_3_ret_to_2; 3386 default: 3387 (void)0; 3388 abort(); 3389 } 3390} 3391static int echo_int_3_i_to_1; 3392static int echo_int_3_i_to_2; 3393static int *get_echo_int_3_i_to(void) __attribute__((__unused__)); 3394static int *get_echo_int_3_i_to(void) { 3395 switch (camkes_get_tls()->thread_index) { 3396 case 1: 3397 return &echo_int_3_i_to_1; 3398 case 2: 3399 return &echo_int_3_i_to_2; 3400 default: 3401 (void)0; 3402 abort(); 3403 } 3404} 3405static char echo_int_3_j_to_1; 3406static char echo_int_3_j_to_2; 3407static char *get_echo_int_3_j_to(void) __attribute__((__unused__)); 3408static char *get_echo_int_3_j_to(void) { 3409 switch (camkes_get_tls()->thread_index) { 3410 case 1: 3411 return &echo_int_3_j_to_1; 3412 case 2: 3413 return &echo_int_3_j_to_2; 3414 default: 3415 (void)0; 3416 abort(); 3417 } 3418} 3419extern void RPCTo_increment_64(uint64_t *x); 3420static unsigned int 3421increment_64_unmarshal_inputs_x(unsigned int _camkes_size_433, 3422 unsigned int _camkes_offset_434, uint64_t *x) { 3423 void *_camkes_buffer_base_435 __attribute__((__unused__)) = 3424 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3425 do { 3426 (void)0; 3427 if (!(!(_camkes_offset_434 + sizeof(*x) > _camkes_size_433))) { 3428 for (;;) 3429 ; 3430 } 3431 } while (0); 3432 memcpy(x, _camkes_buffer_base_435 + _camkes_offset_434, sizeof(*x)); 3433 _camkes_offset_434 += sizeof(*x); 3434 return _camkes_offset_434; 3435} 3436static int increment_64_unmarshal_inputs(unsigned int _camkes_size_436, 3437 uint64_t *x) { 3438 unsigned int _camkes_length_437 __attribute__((__unused__)) = 0; 3439 void *_camkes_buffer_base_438 __attribute__((__unused__)) = 3440 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3441 /* Step over the method index. */ 3442 _camkes_length_437 += sizeof(uint8_t); 3443 /* Unmarshal input parameters. */ 3444 _camkes_length_437 = 3445 increment_64_unmarshal_inputs_x(_camkes_size_436, _camkes_length_437, x); 3446 if (_camkes_length_437 == 0xffffffffU) { 3447 return -1; 3448 } 3449 do { 3450 (void)0; 3451 if (!(!(((_camkes_length_437) + 3452 ((_camkes_length_437) % (sizeof(seL4_Word)) == 0 3453 ? 0 3454 : ((sizeof(seL4_Word)) - 3455 ((_camkes_length_437) % (sizeof(seL4_Word)))))) != 3456 _camkes_size_436))) { 3457 for (;;) 3458 ; 3459 } 3460 } while (0); 3461 return 0; 3462} 3463static unsigned int 3464increment_64_marshal_outputs_x(unsigned int _camkes_offset_440, uint64_t *x) { 3465 void *_camkes_buffer_base_441 __attribute__((__unused__)) = 3466 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3467 do { 3468 (void)0; 3469 if (!(!(_camkes_offset_440 + sizeof(*x) > 3470 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3471 for (;;) 3472 ; 3473 } 3474 } while (0); 3475 memcpy(_camkes_buffer_base_441 + _camkes_offset_440, x, sizeof(*x)); 3476 _camkes_offset_440 += sizeof(*x); 3477 return _camkes_offset_440; 3478} 3479static unsigned int increment_64_marshal_outputs(uint64_t *x) { 3480 unsigned int _camkes_length_443 = 0; 3481 /* Marshal output parameters. */ 3482 _camkes_length_443 = increment_64_marshal_outputs_x(_camkes_length_443, x); 3483 if (_camkes_length_443 == 0xffffffffU) { 3484 return 0xffffffffU; 3485 } 3486 (void)0; 3487 return _camkes_length_443; 3488} 3489static uint64_t increment_64_x_to_1; 3490static uint64_t increment_64_x_to_2; 3491static uint64_t *get_increment_64_x_to(void) __attribute__((__unused__)); 3492static uint64_t *get_increment_64_x_to(void) { 3493 switch (camkes_get_tls()->thread_index) { 3494 case 1: 3495 return &increment_64_x_to_1; 3496 case 2: 3497 return &increment_64_x_to_2; 3498 default: 3499 (void)0; 3500 abort(); 3501 } 3502} 3503extern int RPCTo_echo_int_4(int i, int64_t j, int k, int l); 3504static unsigned int 3505echo_int_4_unmarshal_inputs_i(unsigned int _camkes_size_444, 3506 unsigned int _camkes_offset_445, int *i) { 3507 void *_camkes_buffer_base_446 __attribute__((__unused__)) = 3508 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3509 do { 3510 (void)0; 3511 if (!(!(_camkes_offset_445 + sizeof(*i) > _camkes_size_444))) { 3512 for (;;) 3513 ; 3514 } 3515 } while (0); 3516 memcpy(i, _camkes_buffer_base_446 + _camkes_offset_445, sizeof(*i)); 3517 _camkes_offset_445 += sizeof(*i); 3518 return _camkes_offset_445; 3519} 3520static unsigned int 3521echo_int_4_unmarshal_inputs_j(unsigned int _camkes_size_447, 3522 unsigned int _camkes_offset_448, int64_t *j) { 3523 void *_camkes_buffer_base_449 __attribute__((__unused__)) = 3524 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3525 do { 3526 (void)0; 3527 if (!(!(_camkes_offset_448 + sizeof(*j) > _camkes_size_447))) { 3528 for (;;) 3529 ; 3530 } 3531 } while (0); 3532 memcpy(j, _camkes_buffer_base_449 + _camkes_offset_448, sizeof(*j)); 3533 _camkes_offset_448 += sizeof(*j); 3534 return _camkes_offset_448; 3535} 3536static unsigned int 3537echo_int_4_unmarshal_inputs_k(unsigned int _camkes_size_450, 3538 unsigned int _camkes_offset_451, int *k) { 3539 void *_camkes_buffer_base_452 __attribute__((__unused__)) = 3540 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3541 do { 3542 (void)0; 3543 if (!(!(_camkes_offset_451 + sizeof(*k) > _camkes_size_450))) { 3544 for (;;) 3545 ; 3546 } 3547 } while (0); 3548 memcpy(k, _camkes_buffer_base_452 + _camkes_offset_451, sizeof(*k)); 3549 _camkes_offset_451 += sizeof(*k); 3550 return _camkes_offset_451; 3551} 3552static unsigned int 3553echo_int_4_unmarshal_inputs_l(unsigned int _camkes_size_453, 3554 unsigned int _camkes_offset_454, int *l) { 3555 void *_camkes_buffer_base_455 __attribute__((__unused__)) = 3556 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3557 do { 3558 (void)0; 3559 if (!(!(_camkes_offset_454 + sizeof(*l) > _camkes_size_453))) { 3560 for (;;) 3561 ; 3562 } 3563 } while (0); 3564 memcpy(l, _camkes_buffer_base_455 + _camkes_offset_454, sizeof(*l)); 3565 _camkes_offset_454 += sizeof(*l); 3566 return _camkes_offset_454; 3567} 3568static int echo_int_4_unmarshal_inputs(unsigned int _camkes_size_456, int *i, 3569 int64_t *j, int *k, int *l) { 3570 unsigned int _camkes_length_457 __attribute__((__unused__)) = 0; 3571 void *_camkes_buffer_base_458 __attribute__((__unused__)) = 3572 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3573 /* Step over the method index. */ 3574 _camkes_length_457 += sizeof(uint8_t); 3575 /* Unmarshal input parameters. */ 3576 _camkes_length_457 = 3577 echo_int_4_unmarshal_inputs_i(_camkes_size_456, _camkes_length_457, i); 3578 if (_camkes_length_457 == 0xffffffffU) { 3579 return -1; 3580 } 3581 _camkes_length_457 = 3582 echo_int_4_unmarshal_inputs_j(_camkes_size_456, _camkes_length_457, j); 3583 if (_camkes_length_457 == 0xffffffffU) { 3584 return -1; 3585 } 3586 _camkes_length_457 = 3587 echo_int_4_unmarshal_inputs_k(_camkes_size_456, _camkes_length_457, k); 3588 if (_camkes_length_457 == 0xffffffffU) { 3589 return -1; 3590 } 3591 _camkes_length_457 = 3592 echo_int_4_unmarshal_inputs_l(_camkes_size_456, _camkes_length_457, l); 3593 if (_camkes_length_457 == 0xffffffffU) { 3594 return -1; 3595 } 3596 do { 3597 (void)0; 3598 if (!(!(((_camkes_length_457) + 3599 ((_camkes_length_457) % (sizeof(seL4_Word)) == 0 3600 ? 0 3601 : ((sizeof(seL4_Word)) - 3602 ((_camkes_length_457) % (sizeof(seL4_Word)))))) != 3603 _camkes_size_456))) { 3604 for (;;) 3605 ; 3606 } 3607 } while (0); 3608 return 0; 3609} 3610static unsigned int 3611echo_int_4_marshal_outputs__camkes_ret_fn_459(unsigned int _camkes_offset_460, 3612 int *_camkes_return_461) { 3613 void *_camkes_buffer_base_462 __attribute__((__unused__)) = 3614 (void *)(((void *)&seL4_GetIPCBuffer()->msg[0])); 3615 /* Marshal the return value. */ 3616 do { 3617 (void)0; 3618 if (!(!(_camkes_offset_460 + sizeof(*_camkes_return_461) > 3619 seL4_MsgMaxLength * sizeof(seL4_Word)))) { 3620 for (;;) 3621 ; 3622 } 3623 } while (0); 3624 memcpy(_camkes_buffer_base_462 + _camkes_offset_460, _camkes_return_461, 3625 sizeof(*_camkes_return_461)); 3626 _camkes_offset_460 += sizeof(*_camkes_return_461); 3627 return _camkes_offset_460; 3628} 3629static unsigned int echo_int_4_marshal_outputs(int *_camkes_return_463) { 3630 unsigned int _camkes_length_464 = 0; 3631 _camkes_length_464 = echo_int_4_marshal_outputs__camkes_ret_fn_459( 3632 _camkes_length_464, _camkes_return_463); 3633 if (_camkes_length_464 == 0xffffffffU) { 3634 return 0xffffffffU; 3635 } 3636 /* Marshal output parameters. */ 3637 (void)0; 3638 return _camkes_length_464; 3639} 3640static int echo_int_4_ret_to_1; 3641static int echo_int_4_ret_to_2; 3642static int *get_echo_int_4_ret_to(void) __attribute__((__unused__)); 3643static int *get_echo_int_4_ret_to(void) { 3644 switch (camkes_get_tls()->thread_index) { 3645 case 1: 3646 return &echo_int_4_ret_to_1; 3647 case 2: 3648 return &echo_int_4_ret_to_2; 3649 default: 3650 (void)0; 3651 abort(); 3652 } 3653} 3654static int echo_int_4_i_to_1; 3655static int echo_int_4_i_to_2; 3656static int *get_echo_int_4_i_to(void) __attribute__((__unused__)); 3657static int *get_echo_int_4_i_to(void) { 3658 switch (camkes_get_tls()->thread_index) { 3659 case 1: 3660 return &echo_int_4_i_to_1; 3661 case 2: 3662 return &echo_int_4_i_to_2; 3663 default: 3664 (void)0; 3665 abort(); 3666 } 3667} 3668static int64_t echo_int_4_j_to_1; 3669static int64_t echo_int_4_j_to_2; 3670static int64_t *get_echo_int_4_j_to(void) __attribute__((__unused__)); 3671static int64_t *get_echo_int_4_j_to(void) { 3672 switch (camkes_get_tls()->thread_index) { 3673 case 1: 3674 return &echo_int_4_j_to_1; 3675 case 2: 3676 return &echo_int_4_j_to_2; 3677 default: 3678 (void)0; 3679 abort(); 3680 } 3681} 3682static int echo_int_4_k_to_1; 3683static int echo_int_4_k_to_2; 3684static int *get_echo_int_4_k_to(void) __attribute__((__unused__)); 3685static int *get_echo_int_4_k_to(void) { 3686 switch (camkes_get_tls()->thread_index) { 3687 case 1: 3688 return &echo_int_4_k_to_1; 3689 case 2: 3690 return &echo_int_4_k_to_2; 3691 default: 3692 (void)0; 3693 abort(); 3694 } 3695} 3696static int echo_int_4_l_to_1; 3697static int echo_int_4_l_to_2; 3698static int *get_echo_int_4_l_to(void) __attribute__((__unused__)); 3699static int *get_echo_int_4_l_to(void) { 3700 switch (camkes_get_tls()->thread_index) { 3701 case 1: 3702 return &echo_int_4_l_to_1; 3703 case 2: 3704 return &echo_int_4_l_to_2; 3705 default: 3706 (void)0; 3707 abort(); 3708 } 3709} 3710static uint8_t _camkes_call_tls_var_to_465_1; 3711static uint8_t _camkes_call_tls_var_to_465_2; 3712static uint8_t *get__camkes_call_tls_var_to_465(void) 3713 __attribute__((__unused__)); 3714static uint8_t *get__camkes_call_tls_var_to_465(void) { 3715 switch (camkes_get_tls()->thread_index) { 3716 case 1: 3717 return &_camkes_call_tls_var_to_465_1; 3718 case 2: 3719 return &_camkes_call_tls_var_to_465_2; 3720 default: 3721 (void)0; 3722 abort(); 3723 } 3724} 3725int RPCTo__run(void) { 3726 while (1) { 3727 seL4_MessageInfo_t _camkes_info_466 = seL4_Wait(6, ((void *)0)); 3728 unsigned int _camkes_size_467 = 3729 seL4_MessageInfo_get_length(_camkes_info_466) * sizeof(seL4_Word); 3730 (void)0; 3731 void *_camkes_buffer_468 __attribute__((__unused__)) = 3732 ((void *)&seL4_GetIPCBuffer()->msg[0]); 3733 uint8_t _camkes_call_469 __attribute__((__unused__)); 3734 uint8_t *_camkes_call_ptr_470 = (get__camkes_call_tls_var_to_465()); 3735 do { 3736 (void)0; 3737 if (!(!(sizeof(*_camkes_call_ptr_470) > _camkes_size_467))) { 3738 for (;;) 3739 ; 3740 } 3741 } while (0); 3742 memcpy(_camkes_call_ptr_470, _camkes_buffer_468, 3743 sizeof(*_camkes_call_ptr_470)); 3744 switch (*_camkes_call_ptr_470) { 3745 case 0: { 3746 /* echo_int */ 3747 int i __attribute__((__unused__)); 3748 int *i_ptr = (get_echo_int_i_to()); 3749 /* Unmarshal parameters */ 3750 int _camkes_error_471 = 3751 echo_int_unmarshal_inputs(_camkes_size_467, i_ptr); 3752 if (__builtin_expect(!!(_camkes_error_471 != 0), 0)) { 3753 /* Error in unmarshalling; return to event loop. */ 3754 continue; 3755 } 3756 /* Call the implementation */ 3757 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3758 int _camkes_ret_472 __attribute__((__unused__)); 3759 int *_camkes_ret_ptr_474 = (get_echo_int_ret_to()); 3760 *_camkes_ret_ptr_474 = RPCTo_echo_int(*i_ptr); 3761 /* Marshal the response */ 3762 unsigned int _camkes_length_475 = 3763 echo_int_marshal_outputs(_camkes_ret_ptr_474); 3764 if (__builtin_expect(!!(_camkes_length_475 == 0xffffffffU), 0)) { 3765 /* Error occurred in unmarshalling; return to event loop. */ 3766 continue; 3767 } 3768 _camkes_info_466 = seL4_MessageInfo_new( 3769 0, 0, 0, 3770 /* length */ 3771 ((_camkes_length_475) + 3772 ((_camkes_length_475) % (sizeof(seL4_Word)) == 0 3773 ? 0 3774 : ((sizeof(seL4_Word)) - 3775 ((_camkes_length_475) % (sizeof(seL4_Word)))))) / 3776 sizeof(seL4_Word)); 3777 /* Send the response */ 3778 seL4_Send(6, _camkes_info_466); 3779 break; 3780 } 3781 case 1: { 3782 /* echo_int_1 */ 3783 int i __attribute__((__unused__)); 3784 int *i_ptr = (get_echo_int_1_i_to()); 3785 unsigned int j __attribute__((__unused__)); 3786 unsigned int *j_ptr = (get_echo_int_1_j_to()); 3787 int32_t k __attribute__((__unused__)); 3788 int32_t *k_ptr = (get_echo_int_1_k_to()); 3789 uint32_t l __attribute__((__unused__)); 3790 uint32_t *l_ptr = (get_echo_int_1_l_to()); 3791 /* Unmarshal parameters */ 3792 int _camkes_error_476 = echo_int_1_unmarshal_inputs( 3793 _camkes_size_467, i_ptr, j_ptr, k_ptr, l_ptr); 3794 if (__builtin_expect(!!(_camkes_error_476 != 0), 0)) { 3795 /* Error in unmarshalling; return to event loop. */ 3796 continue; 3797 } 3798 /* Call the implementation */ 3799 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3800 int _camkes_ret_477 __attribute__((__unused__)); 3801 int *_camkes_ret_ptr_479 = (get_echo_int_1_ret_to()); 3802 *_camkes_ret_ptr_479 = RPCTo_echo_int_1(*i_ptr, *j_ptr, *k_ptr, *l_ptr); 3803 /* Marshal the response */ 3804 unsigned int _camkes_length_480 = 3805 echo_int_1_marshal_outputs(_camkes_ret_ptr_479); 3806 if (__builtin_expect(!!(_camkes_length_480 == 0xffffffffU), 0)) { 3807 /* Error occurred in unmarshalling; return to event loop. */ 3808 continue; 3809 } 3810 _camkes_info_466 = seL4_MessageInfo_new( 3811 0, 0, 0, 3812 /* length */ 3813 ((_camkes_length_480) + 3814 ((_camkes_length_480) % (sizeof(seL4_Word)) == 0 3815 ? 0 3816 : ((sizeof(seL4_Word)) - 3817 ((_camkes_length_480) % (sizeof(seL4_Word)))))) / 3818 sizeof(seL4_Word)); 3819 /* Send the response */ 3820 seL4_Send(6, _camkes_info_466); 3821 break; 3822 } 3823 case 2: { 3824 /* echo_parameter */ 3825 int pin __attribute__((__unused__)); 3826 int *pin_ptr = (get_echo_parameter_pin_to()); 3827 int pout __attribute__((__unused__)); 3828 int *pout_ptr = (get_echo_parameter_pout_to()); 3829 /* Unmarshal parameters */ 3830 int _camkes_error_481 = 3831 echo_parameter_unmarshal_inputs(_camkes_size_467, pin_ptr); 3832 if (__builtin_expect(!!(_camkes_error_481 != 0), 0)) { 3833 /* Error in unmarshalling; return to event loop. */ 3834 continue; 3835 } 3836 /* Call the implementation */ 3837 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3838 int _camkes_ret_482 __attribute__((__unused__)); 3839 int *_camkes_ret_ptr_484 = (get_echo_parameter_ret_to()); 3840 *_camkes_ret_ptr_484 = RPCTo_echo_parameter(*pin_ptr, pout_ptr); 3841 /* Marshal the response */ 3842 unsigned int _camkes_length_485 = 3843 echo_parameter_marshal_outputs(_camkes_ret_ptr_484, pout_ptr); 3844 if (__builtin_expect(!!(_camkes_length_485 == 0xffffffffU), 0)) { 3845 /* Error occurred in unmarshalling; return to event loop. */ 3846 continue; 3847 } 3848 _camkes_info_466 = seL4_MessageInfo_new( 3849 0, 0, 0, 3850 /* length */ 3851 ((_camkes_length_485) + 3852 ((_camkes_length_485) % (sizeof(seL4_Word)) == 0 3853 ? 0 3854 : ((sizeof(seL4_Word)) - 3855 ((_camkes_length_485) % (sizeof(seL4_Word)))))) / 3856 sizeof(seL4_Word)); 3857 /* Send the response */ 3858 seL4_Send(6, _camkes_info_466); 3859 break; 3860 } 3861 case 3: { 3862 /* echo_char */ 3863 char i __attribute__((__unused__)); 3864 char *i_ptr = (get_echo_char_i_to()); 3865 /* Unmarshal parameters */ 3866 int _camkes_error_486 = 3867 echo_char_unmarshal_inputs(_camkes_size_467, i_ptr); 3868 if (__builtin_expect(!!(_camkes_error_486 != 0), 0)) { 3869 /* Error in unmarshalling; return to event loop. */ 3870 continue; 3871 } 3872 /* Call the implementation */ 3873 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3874 int _camkes_ret_487 __attribute__((__unused__)); 3875 int *_camkes_ret_ptr_489 = (get_echo_char_ret_to()); 3876 *_camkes_ret_ptr_489 = RPCTo_echo_char(*i_ptr); 3877 /* Marshal the response */ 3878 unsigned int _camkes_length_490 = 3879 echo_char_marshal_outputs(_camkes_ret_ptr_489); 3880 if (__builtin_expect(!!(_camkes_length_490 == 0xffffffffU), 0)) { 3881 /* Error occurred in unmarshalling; return to event loop. */ 3882 continue; 3883 } 3884 _camkes_info_466 = seL4_MessageInfo_new( 3885 0, 0, 0, 3886 /* length */ 3887 ((_camkes_length_490) + 3888 ((_camkes_length_490) % (sizeof(seL4_Word)) == 0 3889 ? 0 3890 : ((sizeof(seL4_Word)) - 3891 ((_camkes_length_490) % (sizeof(seL4_Word)))))) / 3892 sizeof(seL4_Word)); 3893 /* Send the response */ 3894 seL4_Send(6, _camkes_info_466); 3895 break; 3896 } 3897 case 4: { 3898 /* increment_char */ 3899 char x __attribute__((__unused__)); 3900 char *x_ptr = (get_increment_char_x_to()); 3901 /* Unmarshal parameters */ 3902 int _camkes_error_491 = 3903 increment_char_unmarshal_inputs(_camkes_size_467, x_ptr); 3904 if (__builtin_expect(!!(_camkes_error_491 != 0), 0)) { 3905 /* Error in unmarshalling; return to event loop. */ 3906 continue; 3907 } 3908 /* Call the implementation */ 3909 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3910 RPCTo_increment_char(x_ptr); 3911 /* Marshal the response */ 3912 unsigned int _camkes_length_495 = increment_char_marshal_outputs(x_ptr); 3913 if (__builtin_expect(!!(_camkes_length_495 == 0xffffffffU), 0)) { 3914 /* Error occurred in unmarshalling; return to event loop. */ 3915 continue; 3916 } 3917 _camkes_info_466 = seL4_MessageInfo_new( 3918 0, 0, 0, 3919 /* length */ 3920 ((_camkes_length_495) + 3921 ((_camkes_length_495) % (sizeof(seL4_Word)) == 0 3922 ? 0 3923 : ((sizeof(seL4_Word)) - 3924 ((_camkes_length_495) % (sizeof(seL4_Word)))))) / 3925 sizeof(seL4_Word)); 3926 /* Send the response */ 3927 seL4_Send(6, _camkes_info_466); 3928 break; 3929 } 3930 case 5: { 3931 /* increment_parameter */ 3932 int x __attribute__((__unused__)); 3933 int *x_ptr = (get_increment_parameter_x_to()); 3934 /* Unmarshal parameters */ 3935 int _camkes_error_496 = 3936 increment_parameter_unmarshal_inputs(_camkes_size_467, x_ptr); 3937 if (__builtin_expect(!!(_camkes_error_496 != 0), 0)) { 3938 /* Error in unmarshalling; return to event loop. */ 3939 continue; 3940 } 3941 /* Call the implementation */ 3942 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3943 RPCTo_increment_parameter(x_ptr); 3944 /* Marshal the response */ 3945 unsigned int _camkes_length_500 = 3946 increment_parameter_marshal_outputs(x_ptr); 3947 if (__builtin_expect(!!(_camkes_length_500 == 0xffffffffU), 0)) { 3948 /* Error occurred in unmarshalling; return to event loop. */ 3949 continue; 3950 } 3951 _camkes_info_466 = seL4_MessageInfo_new( 3952 0, 0, 0, 3953 /* length */ 3954 ((_camkes_length_500) + 3955 ((_camkes_length_500) % (sizeof(seL4_Word)) == 0 3956 ? 0 3957 : ((sizeof(seL4_Word)) - 3958 ((_camkes_length_500) % (sizeof(seL4_Word)))))) / 3959 sizeof(seL4_Word)); 3960 /* Send the response */ 3961 seL4_Send(6, _camkes_info_466); 3962 break; 3963 } 3964 case 6: { 3965 /* echo_int_2 */ 3966 int i __attribute__((__unused__)); 3967 int *i_ptr = (get_echo_int_2_i_to()); 3968 int j __attribute__((__unused__)); 3969 int *j_ptr = (get_echo_int_2_j_to()); 3970 /* Unmarshal parameters */ 3971 int _camkes_error_501 = 3972 echo_int_2_unmarshal_inputs(_camkes_size_467, i_ptr, j_ptr); 3973 if (__builtin_expect(!!(_camkes_error_501 != 0), 0)) { 3974 /* Error in unmarshalling; return to event loop. */ 3975 continue; 3976 } 3977 /* Call the implementation */ 3978 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 3979 int _camkes_ret_502 __attribute__((__unused__)); 3980 int *_camkes_ret_ptr_504 = (get_echo_int_2_ret_to()); 3981 *_camkes_ret_ptr_504 = RPCTo_echo_int_2(*i_ptr, *j_ptr); 3982 /* Marshal the response */ 3983 unsigned int _camkes_length_505 = 3984 echo_int_2_marshal_outputs(_camkes_ret_ptr_504); 3985 if (__builtin_expect(!!(_camkes_length_505 == 0xffffffffU), 0)) { 3986 /* Error occurred in unmarshalling; return to event loop. */ 3987 continue; 3988 } 3989 _camkes_info_466 = seL4_MessageInfo_new( 3990 0, 0, 0, 3991 /* length */ 3992 ((_camkes_length_505) + 3993 ((_camkes_length_505) % (sizeof(seL4_Word)) == 0 3994 ? 0 3995 : ((sizeof(seL4_Word)) - 3996 ((_camkes_length_505) % (sizeof(seL4_Word)))))) / 3997 sizeof(seL4_Word)); 3998 /* Send the response */ 3999 seL4_Send(6, _camkes_info_466); 4000 break; 4001 } 4002 case 7: { 4003 /* echo_int_3 */ 4004 int i __attribute__((__unused__)); 4005 int *i_ptr = (get_echo_int_3_i_to()); 4006 char j __attribute__((__unused__)); 4007 char *j_ptr = (get_echo_int_3_j_to()); 4008 /* Unmarshal parameters */ 4009 int _camkes_error_506 = 4010 echo_int_3_unmarshal_inputs(_camkes_size_467, i_ptr, j_ptr); 4011 if (__builtin_expect(!!(_camkes_error_506 != 0), 0)) { 4012 /* Error in unmarshalling; return to event loop. */ 4013 continue; 4014 } 4015 /* Call the implementation */ 4016 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 4017 int _camkes_ret_507 __attribute__((__unused__)); 4018 int *_camkes_ret_ptr_509 = (get_echo_int_3_ret_to()); 4019 *_camkes_ret_ptr_509 = RPCTo_echo_int_3(*i_ptr, *j_ptr); 4020 /* Marshal the response */ 4021 unsigned int _camkes_length_510 = 4022 echo_int_3_marshal_outputs(_camkes_ret_ptr_509); 4023 if (__builtin_expect(!!(_camkes_length_510 == 0xffffffffU), 0)) { 4024 /* Error occurred in unmarshalling; return to event loop. */ 4025 continue; 4026 } 4027 _camkes_info_466 = seL4_MessageInfo_new( 4028 0, 0, 0, 4029 /* length */ 4030 ((_camkes_length_510) + 4031 ((_camkes_length_510) % (sizeof(seL4_Word)) == 0 4032 ? 0 4033 : ((sizeof(seL4_Word)) - 4034 ((_camkes_length_510) % (sizeof(seL4_Word)))))) / 4035 sizeof(seL4_Word)); 4036 /* Send the response */ 4037 seL4_Send(6, _camkes_info_466); 4038 break; 4039 } 4040 case 8: { 4041 /* increment_64 */ 4042 uint64_t x __attribute__((__unused__)); 4043 uint64_t *x_ptr = (get_increment_64_x_to()); 4044 /* Unmarshal parameters */ 4045 int _camkes_error_511 = 4046 increment_64_unmarshal_inputs(_camkes_size_467, x_ptr); 4047 if (__builtin_expect(!!(_camkes_error_511 != 0), 0)) { 4048 /* Error in unmarshalling; return to event loop. */ 4049 continue; 4050 } 4051 /* Call the implementation */ 4052 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 4053 RPCTo_increment_64(x_ptr); 4054 /* Marshal the response */ 4055 unsigned int _camkes_length_515 = increment_64_marshal_outputs(x_ptr); 4056 if (__builtin_expect(!!(_camkes_length_515 == 0xffffffffU), 0)) { 4057 /* Error occurred in unmarshalling; return to event loop. */ 4058 continue; 4059 } 4060 _camkes_info_466 = seL4_MessageInfo_new( 4061 0, 0, 0, 4062 /* length */ 4063 ((_camkes_length_515) + 4064 ((_camkes_length_515) % (sizeof(seL4_Word)) == 0 4065 ? 0 4066 : ((sizeof(seL4_Word)) - 4067 ((_camkes_length_515) % (sizeof(seL4_Word)))))) / 4068 sizeof(seL4_Word)); 4069 /* Send the response */ 4070 seL4_Send(6, _camkes_info_466); 4071 break; 4072 } 4073 case 9: { 4074 /* echo_int_4 */ 4075 int i __attribute__((__unused__)); 4076 int *i_ptr = (get_echo_int_4_i_to()); 4077 int64_t j __attribute__((__unused__)); 4078 int64_t *j_ptr = (get_echo_int_4_j_to()); 4079 int k __attribute__((__unused__)); 4080 int *k_ptr = (get_echo_int_4_k_to()); 4081 int l __attribute__((__unused__)); 4082 int *l_ptr = (get_echo_int_4_l_to()); 4083 /* Unmarshal parameters */ 4084 int _camkes_error_516 = echo_int_4_unmarshal_inputs( 4085 _camkes_size_467, i_ptr, j_ptr, k_ptr, l_ptr); 4086 if (__builtin_expect(!!(_camkes_error_516 != 0), 0)) { 4087 /* Error in unmarshalling; return to event loop. */ 4088 continue; 4089 } 4090 /* Call the implementation */ 4091 /*_ set ret_sz_ptr = c_symbol('ret_sz_ptr') -*/ 4092 int _camkes_ret_517 __attribute__((__unused__)); 4093 int *_camkes_ret_ptr_519 = (get_echo_int_4_ret_to()); 4094 *_camkes_ret_ptr_519 = RPCTo_echo_int_4(*i_ptr, *j_ptr, *k_ptr, *l_ptr); 4095 /* Marshal the response */ 4096 unsigned int _camkes_length_520 = 4097 echo_int_4_marshal_outputs(_camkes_ret_ptr_519); 4098 if (__builtin_expect(!!(_camkes_length_520 == 0xffffffffU), 0)) { 4099 /* Error occurred in unmarshalling; return to event loop. */ 4100 continue; 4101 } 4102 _camkes_info_466 = seL4_MessageInfo_new( 4103 0, 0, 0, 4104 /* length */ 4105 ((_camkes_length_520) + 4106 ((_camkes_length_520) % (sizeof(seL4_Word)) == 0 4107 ? 0 4108 : ((sizeof(seL4_Word)) - 4109 ((_camkes_length_520) % (sizeof(seL4_Word)))))) / 4110 sizeof(seL4_Word)); 4111 /* Send the response */ 4112 seL4_Send(6, _camkes_info_466); 4113 break; 4114 } 4115 default: { 4116 do { 4117 (void)0; 4118 if (!(0)) { 4119 for (;;) 4120 ; 4121 } 4122 } while (0); 4123 } 4124 } 4125 } 4126 do { 4127 (void)0; 4128 __builtin_unreachable(); 4129 } while (0); 4130} 4131