/* * Copyright 2014, NICTA * * This software may be distributed and modified according to the terms of * the GNU General Public License version 2. Note that NO WARRANTY is provided. * See "LICENSE_GPLv2.txt" for details. * * @TAG(NICTA_GPL) */ typedef unsigned size_t ; typedef int ptrdiff_t ; typedef unsigned wchar_t ; typedef signed char int8_t ; typedef short int16_t ; typedef int int32_t ; typedef long long int64_t ; typedef unsigned char uint8_t ; typedef unsigned short uint16_t ; typedef unsigned int uint32_t ; typedef unsigned long long uint64_t ; typedef int8_t int_fast8_t ; typedef int int_fast16_t ; typedef int int_fast32_t ; typedef int64_t int_fast64_t ; typedef unsigned char uint_fast8_t ; typedef unsigned int uint_fast16_t ; typedef unsigned int uint_fast32_t ; typedef uint64_t uint_fast64_t ; typedef long intptr_t ; typedef unsigned long uintptr_t ; typedef int8_t int_least8_t ; typedef int16_t int_least16_t ; typedef int32_t int_least32_t ; typedef int64_t int_least64_t ; typedef uint8_t uint_least8_t ; typedef uint16_t uint_least16_t ; typedef uint32_t uint_least32_t ; typedef uint64_t uint_least64_t ; typedef long long intmax_t ; typedef unsigned long long uintmax_t ; typedef uint32_t seL4_Word ; typedef seL4_Word seL4_CPtr ; typedef seL4_CPtr seL4_ARM_Page ; typedef seL4_CPtr seL4_ARM_PageTable ; typedef seL4_CPtr seL4_ARM_PageDirectory ; typedef seL4_CPtr seL4_ARM_ASIDControl ; typedef seL4_CPtr seL4_ARM_ASIDPool ; typedef struct { /* frame registers */ seL4_Word pc , sp , cpsr , r0 , r1 , r8 , r9 , r10 , r11 , r12 ; /* other integer registers */ seL4_Word r2 , r3 , r4 , r5 , r6 , r7 , r14 ; } seL4_UserContext ; typedef enum { seL4_ARM_PageCacheable = 0x01 , seL4_ARM_ParityEnabled = 0x02 , seL4_ARM_Default_VMAttributes = 0x03 , /* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */ _enum_pad_seL4_ARM_VMAttributes = ( 1U << ( ( sizeof ( int ) * 8 ) - 1 ) ) , } seL4_ARM_VMAttributes ; struct seL4_MessageInfo { uint32_t words [ 1 ] ; } ; typedef struct seL4_MessageInfo seL4_MessageInfo_t ; static inline seL4_MessageInfo_t __attribute__ ( ( __const__ ) ) seL4_MessageInfo_new ( uint32_t label , uint32_t capsUnwrapped , uint32_t extraCaps , uint32_t length ) { seL4_MessageInfo_t seL4_MessageInfo ; seL4_MessageInfo . words [ 0 ] = 0 ; seL4_MessageInfo . words [ 0 ] |= ( label & 0xfffff ) << 12 ; seL4_MessageInfo . words [ 0 ] |= ( capsUnwrapped & 0x7 ) << 9 ; seL4_MessageInfo . words [ 0 ] |= ( extraCaps & 0x3 ) << 7 ; seL4_MessageInfo . words [ 0 ] |= ( length & 0x7f ) << 0 ; return seL4_MessageInfo ; } struct seL4_CapData { uint32_t words [ 1 ] ; } ; typedef struct seL4_CapData seL4_CapData_t ; enum seL4_CapData_tag { seL4_CapData_Badge = 0 , seL4_CapData_Guard = 1 } ; typedef enum seL4_CapData_tag seL4_CapData_tag_t ; typedef enum { seL4_SysCall = - 1 , seL4_SysReplyWait = - 2 , seL4_SysSend = - 3 , seL4_SysNBSend = - 4 , seL4_SysWait = - 5 , seL4_SysReply = - 6 , seL4_SysYield = - 7 , seL4_SysPoll = - 8 , seL4_SysDebugPutChar = - 9 , seL4_SysDebugHalt = - 10 , seL4_SysDebugCapIdentify = - 11 , seL4_SysDebugSnapshot = - 12 , _enum_pad_seL4_Syscall_ID = ( 1U << ( ( sizeof ( int ) * 8 ) - 1 ) ) } seL4_Syscall_ID ; typedef enum api_object { seL4_UntypedObject , seL4_TCBObject , seL4_EndpointObject , seL4_NotificationObject , seL4_CapTableObject , seL4_NonArchObjectTypeCount , } seL4_ObjectType ; typedef uint32_t api_object_t ; typedef enum { seL4_NoError = 0 , seL4_InvalidArgument , seL4_InvalidCapability , seL4_IllegalOperation , seL4_RangeError , seL4_AlignmentError , seL4_FailedLookup , seL4_TruncatedMessage , seL4_DeleteFirst , seL4_RevokeFirst , seL4_NotEnoughMemory , } seL4_Error ; enum priorityConstants { seL4_InvalidPrio = - 1 , seL4_MinPrio = 0 , seL4_MaxPrio = 255 } ; enum seL4_MsgLimits { seL4_MsgLengthBits = 7 , seL4_MsgExtraCapBits = 2 } ; typedef enum { seL4_NoFault = 0 , seL4_CapFault , seL4_VMFault , seL4_UnknownSyscall , seL4_UserException , _enum_pad_seL4_FaultType = ( 1U << ( ( sizeof ( int ) * 8 ) - 1 ) ) , } seL4_FaultType ; typedef enum { seL4_NoFailure = 0 , seL4_InvalidRoot , seL4_MissingCapability , seL4_DepthMismatch , seL4_GuardMismatch , _enum_pad_seL4_LookupFailureType = ( 1U << ( ( sizeof ( int ) * 8 ) - 1 ) ) , } seL4_LookupFailureType ; typedef enum { seL4_CanWrite = 0x01 , seL4_CanRead = 0x02 , seL4_CanGrant = 0x04 , seL4_AllRights = 0x07 , /* seL4_CanWrite | seL4_CanRead | seL4_CanGrant */ seL4_Transfer_Mint = 0x100 , _enum_pad_seL4_CapRights = ( 1U << ( ( sizeof ( int ) * 8 ) - 1 ) ) , } seL4_CapRights ; typedef struct seL4_IPCBuffer_ { seL4_MessageInfo_t tag ; seL4_Word msg [ 120 ] ; seL4_Word userData ; seL4_Word caps_or_badges [ ( ( 1ul << ( seL4_MsgExtraCapBits ) ) - 1 ) ] ; seL4_CPtr receiveCNode ; seL4_CPtr receiveIndex ; seL4_Word receiveDepth ; } seL4_IPCBuffer ; typedef seL4_CPtr seL4_CNode ; typedef seL4_CPtr seL4_IRQHandler ; typedef seL4_CPtr seL4_IRQControl ; typedef seL4_CPtr seL4_TCB ; typedef seL4_CPtr seL4_Untyped ; typedef seL4_CPtr seL4_DomainSet ; typedef enum _object { seL4_ARM_SmallPageObject = seL4_NonArchObjectTypeCount , seL4_ARM_LargePageObject , seL4_ARM_SectionObject , seL4_ARM_SuperSectionObject , seL4_ARM_PageTableObject , seL4_ARM_PageDirectoryObject , seL4_ObjectTypeCount } seL4_ArchObjectType ; typedef uint32_t object_t ; enum invocation_label { InvalidInvocation , UntypedRetype , TCBReadRegisters , TCBWriteRegisters , TCBCopyRegisters , TCBConfigure , TCBSetPriority , TCBSetIPCBuffer , TCBSetSpace , TCBSuspend , TCBResume , TCBBindNotification , TCBUnbindNotification , CNodeRevoke , CNodeDelete , CNodeRecycle , CNodeCopy , CNodeMint , CNodeMove , CNodeMutate , CNodeRotate , CNodeSaveCaller , IRQIssueIRQHandler , IRQInterruptControl , IRQAckIRQ , IRQSetIRQHandler , IRQClearIRQHandler , DomainSetSet , nInvocationLabels } ; enum arch_invocation_label { ARMPDClean_Data = nInvocationLabels + 0 , ARMPDInvalidate_Data = nInvocationLabels + 1 , ARMPDCleanInvalidate_Data = nInvocationLabels + 2 , ARMPDUnify_Instruction = nInvocationLabels + 3 , ARMPageTableMap = nInvocationLabels + 4 , ARMPageTableUnmap = nInvocationLabels + 5 , ARMPageMap = nInvocationLabels + 6 , ARMPageRemap = nInvocationLabels + 7 , ARMPageUnmap = nInvocationLabels + 8 , ARMPageClean_Data = nInvocationLabels + 9 , ARMPageInvalidate_Data = nInvocationLabels + 10 , ARMPageCleanInvalidate_Data = nInvocationLabels + 11 , ARMPageUnify_Instruction = nInvocationLabels + 12 , ARMPageGetAddress = nInvocationLabels + 13 , ARMASIDControlMakePool = nInvocationLabels + 14 , ARMASIDPoolAssign = nInvocationLabels + 15 , nArchInvocationLabels } ; enum { seL4_GlobalsFrame = 0xffffc000 , } ; static inline seL4_IPCBuffer * seL4_GetIPCBuffer ( void ) { return * ( seL4_IPCBuffer * * ) seL4_GlobalsFrame ; } static inline seL4_Word seL4_GetMR ( int i ) { return seL4_GetIPCBuffer ( ) -> msg [ i ] ; } static inline void seL4_SetMR ( int i , seL4_Word mr ) { seL4_GetIPCBuffer ( ) -> msg [ i ] = mr ; } static inline seL4_MessageInfo_t seL4_Wait ( seL4_CPtr src , seL4_Word * sender ) { register seL4_Word src_and_badge asm ( "r0" ) = ( seL4_Word ) src ; register seL4_MessageInfo_t info asm ( "r1" ) ; /* Incoming message registers. */ register seL4_Word msg0 asm ( "r2" ) ; register seL4_Word msg1 asm ( "r3" ) ; register seL4_Word msg2 asm ( "r4" ) ; register seL4_Word msg3 asm ( "r5" ) ; /* Perform the system call. */ register seL4_Word scno asm ( "r7" ) = seL4_SysWait ; asm volatile ( "swi %[swi_num]" : "=r" ( msg0 ) , "=r" ( msg1 ) , "=r" ( msg2 ) , "=r" ( msg3 ) , "=r" ( info ) , "+r" ( src_and_badge ) : [ swi_num ] "i" ( ( seL4_SysWait ) & 0x00ffffff ) , "r" ( scno ) : "memory" ) ; /* Write the message back out to memory. */ seL4_SetMR ( 0 , msg0 ) ; seL4_SetMR ( 1 , msg1 ) ; seL4_SetMR ( 2 , msg2 ) ; seL4_SetMR ( 3 , msg3 ) ; /* Return back sender and message information. */ if ( sender ) { * sender = src_and_badge ; } return info ; } static inline seL4_MessageInfo_t seL4_ReplyWait ( seL4_CPtr src , seL4_MessageInfo_t msgInfo , seL4_Word * sender ) { register seL4_Word src_and_badge asm ( "r0" ) = ( seL4_Word ) src ; register seL4_MessageInfo_t info asm ( "r1" ) = msgInfo ; /* Load beginning of the message into registers. */ register seL4_Word msg0 asm ( "r2" ) = seL4_GetMR ( 0 ) ; register seL4_Word msg1 asm ( "r3" ) = seL4_GetMR ( 1 ) ; register seL4_Word msg2 asm ( "r4" ) = seL4_GetMR ( 2 ) ; register seL4_Word msg3 asm ( "r5" ) = seL4_GetMR ( 3 ) ; /* Perform the syscall. */ register seL4_Word scno asm ( "r7" ) = seL4_SysReplyWait ; asm volatile ( "swi %[swi_num]" : "+r" ( msg0 ) , "+r" ( msg1 ) , "+r" ( msg2 ) , "+r" ( msg3 ) , "+r" ( info ) , "+r" ( src_and_badge ) : [ swi_num ] "i" ( ( seL4_SysReplyWait ) & 0x00ffffff ) , "r" ( scno ) : "memory" ) ; /* Write the message back out to memory. */ seL4_SetMR ( 0 , msg0 ) ; seL4_SetMR ( 1 , msg1 ) ; seL4_SetMR ( 2 , msg2 ) ; seL4_SetMR ( 3 , msg3 ) ; /* Return back sender and message information. */ if ( sender ) { * sender = src_and_badge ; } return info ; } typedef unsigned long __type_uint8_t_size_incorrect [ ( sizeof ( uint8_t ) == 1 ) ? 1 : - 1 ] ; typedef unsigned long __type_uint16_t_size_incorrect [ ( sizeof ( uint16_t ) == 2 ) ? 1 : - 1 ] ; typedef unsigned long __type_uint32_t_size_incorrect [ ( sizeof ( uint32_t ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_uint64_t_size_incorrect [ ( sizeof ( uint64_t ) == 8 ) ? 1 : - 1 ] ; typedef unsigned long __type_int_size_incorrect [ ( sizeof ( int ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_bool_size_incorrect [ ( sizeof ( _Bool ) == 1 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_Word_size_incorrect [ ( sizeof ( seL4_Word ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_CapRights_size_incorrect [ ( sizeof ( seL4_CapRights ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_CapData_t_size_incorrect [ ( sizeof ( seL4_CapData_t ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_CPtr_size_incorrect [ ( sizeof ( seL4_CPtr ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_CNode_size_incorrect [ ( sizeof ( seL4_CNode ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_IRQHandler_size_incorrect [ ( sizeof ( seL4_IRQHandler ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_IRQControl_size_incorrect [ ( sizeof ( seL4_IRQControl ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_TCB_size_incorrect [ ( sizeof ( seL4_TCB ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_Untyped_size_incorrect [ ( sizeof ( seL4_Untyped ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_DomainSet_size_incorrect [ ( sizeof ( seL4_DomainSet ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_VMAttributes_size_incorrect [ ( sizeof ( seL4_ARM_VMAttributes ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_Page_size_incorrect [ ( sizeof ( seL4_ARM_Page ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_PageTable_size_incorrect [ ( sizeof ( seL4_ARM_PageTable ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_PageDirectory_size_incorrect [ ( sizeof ( seL4_ARM_PageDirectory ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_ASIDControl_size_incorrect [ ( sizeof ( seL4_ARM_ASIDControl ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_ARM_ASIDPool_size_incorrect [ ( sizeof ( seL4_ARM_ASIDPool ) == 4 ) ? 1 : - 1 ] ; typedef unsigned long __type_seL4_UserContext_size_incorrect [ ( sizeof ( seL4_UserContext ) == 68 ) ? 1 : - 1 ] ; struct seL4_ARM_Page_GetAddress { int error ; seL4_Word paddr ; } ; typedef struct seL4_ARM_Page_GetAddress seL4_ARM_Page_GetAddress_t ; enum { seL4_CapNull = 0 , /* null cap */ seL4_CapInitThreadTCB = 1 , /* initial thread's TCB cap */ seL4_CapInitThreadCNode = 2 , /* initial thread's root CNode cap */ seL4_CapInitThreadPD = 3 , /* initial thread's PD cap */ seL4_CapIRQControl = 4 , /* global IRQ controller cap */ seL4_CapASIDControl = 5 , /* global ASID controller cap */ seL4_CapInitThreadASIDPool = 6 , /* initial thread's ASID pool cap */ seL4_CapIOPort = 7 , /* global IO port cap (null cap if not supported) */ seL4_CapIOSpace = 8 , /* global IO space cap (null cap if no IOMMU support) */ seL4_CapBootInfoFrame = 9 , /* bootinfo frame cap */ seL4_CapInitThreadIPCBuffer = 10 , /* initial thread's IPC buffer frame cap */ seL4_CapDomain = 11 /* global domain controller cap */ } ; typedef struct { seL4_Word start ; /* first CNode slot position OF region */ seL4_Word end ; /* first CNode slot position AFTER region */ } seL4_SlotRegion ; typedef struct { seL4_Word basePaddr ; /* base physical address of device region */ seL4_Word frameSizeBits ; /* size (2^n bytes) of a device-region frame */ seL4_SlotRegion frames ; /* device-region frame caps */ } seL4_DeviceRegion ; typedef struct { seL4_Word nodeID ; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */ seL4_Word numNodes ; /* number of seL4 nodes (1 if uniprocessor) */ seL4_Word numIOPTLevels ; /* number of IOMMU PT levels (0 if no IOMMU support) */ seL4_IPCBuffer * ipcBuffer ; /* pointer to initial thread's IPC buffer */ seL4_SlotRegion empty ; /* empty slots (null caps) */ seL4_SlotRegion sharedFrames ; /* shared-frame caps (shared between seL4 nodes) */ seL4_SlotRegion userImageFrames ; /* userland-image frame caps */ seL4_SlotRegion userImagePTs ; /* userland-image PT caps */ seL4_SlotRegion untyped ; /* untyped-object caps (untyped caps) */ seL4_Word untypedPaddrList [ 167 ] ; /* physical address of each untyped cap */ uint8_t untypedSizeBitsList [ 167 ] ; /* size (2^n) bytes of each untyped cap */ uint8_t initThreadCNodeSizeBits ; /* initial thread's root CNode size (2^n slots) */ seL4_Word numDeviceRegions ; /* number of device regions */ seL4_DeviceRegion deviceRegions [ 199 ] ; /* device regions */ uint8_t initThreadDomain ; /* Initial thread's domain ID */ } seL4_BootInfo ; typedef struct camkes_tls_t { seL4_CPtr tcb_cap ; unsigned int thread_index ; } camkes_tls_t ; static inline camkes_tls_t * __attribute__ ( ( __unused__ ) ) camkes_get_tls ( void ) { /* We store TLS data in the same page as the thread's IPC buffer, but at * the start of the page. */ uintptr_t ipc_buffer = ( uintptr_t ) seL4_GetIPCBuffer ( ) ; /* Normally we would just use MASK here, but the verification C parser * doesn't like the GCC extension used in that macro. */ typedef char _assertion_failed__static_assert_0 [ ( ( 12 <= 31 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; uintptr_t tls = ipc_buffer & ~ ( ( ( 1ul << ( 12 ) ) - 1ul ) ) ; /* We should have enough room for the TLS data preceding the IPC buffer. */ ( ( void ) 0 ) ; /* We'd better be returning a valid pointer. */ ( ( void ) 0 ) ; return ( camkes_tls_t * ) tls ; } void abort ( void ) ; typedef struct { int quot , rem ; } div_t ; typedef struct { long quot , rem ; } ldiv_t ; typedef struct { long long quot , rem ; } lldiv_t ; extern int RPCTo_echo_int ( int i ) ; extern int RPCTo_echo_parameter ( int pin , int * pout ) ; extern int RPCTo_echo_char ( char i ) ; extern void RPCTo_increment_char ( char * x ) ; extern void RPCTo_increment_parameter ( int * x ) ; extern void RPCTo_increment_64 ( uint64_t * x ) ; static int echo_int_i_1 ; static int echo_int_i_2 ; static int * __attribute__ ( ( unused ) ) get_echo_int_i ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & echo_int_i_1 ; case 2 : return & echo_int_i_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int echo_int_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_27 = 1 ; /* 0 contained the method index. */ int * i = get_echo_int_i ( ) ; typedef char _assertion_failed__static_assert_1 [ ( ( sizeof ( i ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * i = seL4_GetMR ( _camkes_mr_27 ) ; _camkes_mr_27 += 1 ; typedef char _assertion_failed__static_assert_2 [ ( ( _camkes_mr_27 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ int _camkes_ret_28 = RPCTo_echo_int ( * i ) ; /* Marshal the response */ _camkes_mr_27 = 0 ; typedef char _assertion_failed__static_assert_3 [ ( ( sizeof ( _camkes_ret_28 ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_27 , _camkes_ret_28 ) ; _camkes_mr_27 += 1 ; return _camkes_mr_27 ; } static int echo_parameter_pin_1 ; static int echo_parameter_pin_2 ; static int * __attribute__ ( ( unused ) ) get_echo_parameter_pin ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & echo_parameter_pin_1 ; case 2 : return & echo_parameter_pin_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static int echo_parameter_pout_1 ; static int echo_parameter_pout_2 ; static int * __attribute__ ( ( unused ) ) get_echo_parameter_pout ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & echo_parameter_pout_1 ; case 2 : return & echo_parameter_pout_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int echo_parameter_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_29 = 1 ; /* 0 contained the method index. */ int * pin = get_echo_parameter_pin ( ) ; typedef char _assertion_failed__static_assert_4 [ ( ( sizeof ( pin ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * pin = seL4_GetMR ( _camkes_mr_29 ) ; _camkes_mr_29 += 1 ; int * pout = get_echo_parameter_pout ( ) ; typedef char _assertion_failed__static_assert_5 [ ( ( _camkes_mr_29 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ int _camkes_ret_30 = RPCTo_echo_parameter ( * pin , pout ) ; /* Marshal the response */ _camkes_mr_29 = 0 ; typedef char _assertion_failed__static_assert_6 [ ( ( sizeof ( _camkes_ret_30 ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_29 , _camkes_ret_30 ) ; _camkes_mr_29 += 1 ; typedef char _assertion_failed__static_assert_7 [ ( ( sizeof ( pout ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_29 , * pout ) ; _camkes_mr_29 += 1 ; return _camkes_mr_29 ; } static char echo_char_i_1 ; static char echo_char_i_2 ; static char * __attribute__ ( ( unused ) ) get_echo_char_i ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & echo_char_i_1 ; case 2 : return & echo_char_i_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int echo_char_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_31 = 1 ; /* 0 contained the method index. */ char * i = get_echo_char_i ( ) ; typedef char _assertion_failed__static_assert_8 [ ( ( sizeof ( i ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * i = seL4_GetMR ( _camkes_mr_31 ) ; _camkes_mr_31 += 1 ; typedef char _assertion_failed__static_assert_9 [ ( ( _camkes_mr_31 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ int _camkes_ret_32 = RPCTo_echo_char ( * i ) ; /* Marshal the response */ _camkes_mr_31 = 0 ; typedef char _assertion_failed__static_assert_10 [ ( ( sizeof ( _camkes_ret_32 ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_31 , _camkes_ret_32 ) ; _camkes_mr_31 += 1 ; return _camkes_mr_31 ; } static char increment_char_x_1 ; static char increment_char_x_2 ; static char * __attribute__ ( ( unused ) ) get_increment_char_x ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & increment_char_x_1 ; case 2 : return & increment_char_x_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int increment_char_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_33 = 1 ; /* 0 contained the method index. */ char * x = get_increment_char_x ( ) ; typedef char _assertion_failed__static_assert_11 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * x = seL4_GetMR ( _camkes_mr_33 ) ; _camkes_mr_33 += 1 ; typedef char _assertion_failed__static_assert_12 [ ( ( _camkes_mr_33 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ RPCTo_increment_char ( x ) ; /* Marshal the response */ _camkes_mr_33 = 0 ; typedef char _assertion_failed__static_assert_13 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_33 , * x ) ; _camkes_mr_33 += 1 ; return _camkes_mr_33 ; } static int increment_parameter_x_1 ; static int increment_parameter_x_2 ; static int * __attribute__ ( ( unused ) ) get_increment_parameter_x ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & increment_parameter_x_1 ; case 2 : return & increment_parameter_x_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int increment_parameter_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_34 = 1 ; /* 0 contained the method index. */ int * x = get_increment_parameter_x ( ) ; typedef char _assertion_failed__static_assert_14 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * x = seL4_GetMR ( _camkes_mr_34 ) ; _camkes_mr_34 += 1 ; typedef char _assertion_failed__static_assert_15 [ ( ( _camkes_mr_34 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ RPCTo_increment_parameter ( x ) ; /* Marshal the response */ _camkes_mr_34 = 0 ; typedef char _assertion_failed__static_assert_16 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_34 , * x ) ; _camkes_mr_34 += 1 ; return _camkes_mr_34 ; } static uint64_t increment_64_x_1 ; static uint64_t increment_64_x_2 ; static uint64_t * __attribute__ ( ( unused ) ) get_increment_64_x ( void ) { switch ( camkes_get_tls ( ) -> thread_index ) { case 1 : return & increment_64_x_1 ; case 2 : return & increment_64_x_2 ; default : ( ( void ) 0 ) ; abort ( ) ; } } static unsigned int increment_64_internal ( void ) { /* Unmarshal parameters */ unsigned int _camkes_mr_35 = 1 ; /* 0 contained the method index. */ uint64_t * x = get_increment_64_x ( ) ; typedef char _assertion_failed__static_assert_17 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; * x = seL4_GetMR ( _camkes_mr_35 ) ; _camkes_mr_35 += 1 ; /* We need a second message register. */ * x |= ( ( uint64_t ) seL4_GetMR ( _camkes_mr_35 ) ) << ( sizeof ( seL4_Word ) * 8 ) ; _camkes_mr_35 += 1 ; typedef char _assertion_failed__static_assert_18 [ ( ( _camkes_mr_35 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Call the implementation */ RPCTo_increment_64 ( x ) ; /* Marshal the response */ _camkes_mr_35 = 0 ; typedef char _assertion_failed__static_assert_19 [ ( ( sizeof ( x ) <= 2 * sizeof ( seL4_Word ) ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; seL4_SetMR ( _camkes_mr_35 , * x ) ; _camkes_mr_35 += 1 ; /* We need a second message register. */ seL4_SetMR ( _camkes_mr_35 , ( seL4_Word ) ( * x >> ( sizeof ( seL4_Word ) * 8 ) ) ) ; _camkes_mr_35 += 1 ; return _camkes_mr_35 ; } static seL4_MessageInfo_t RPCTo__run_internal ( _Bool _camkes_first_37 , seL4_MessageInfo_t _camkes_info_36 ) { if ( _camkes_first_37 ) { _camkes_info_36 = seL4_Wait ( 6 , ( ( void * ) 0 ) ) ; } /* We should have at least been passed a method index */ ( ( void ) 0 ) ; int _camkes_call_38 = ( int ) seL4_GetMR ( 0 ) ; switch ( _camkes_call_38 ) { case 0 : { /* echo_int */ unsigned int _camkes_length_39 = echo_int_internal ( ) ; typedef char _assertion_failed__static_assert_20 [ ( ( _camkes_length_39 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_39 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } case 1 : { /* echo_parameter */ unsigned int _camkes_length_40 = echo_parameter_internal ( ) ; typedef char _assertion_failed__static_assert_21 [ ( ( _camkes_length_40 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_40 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } case 2 : { /* echo_char */ unsigned int _camkes_length_41 = echo_char_internal ( ) ; typedef char _assertion_failed__static_assert_22 [ ( ( _camkes_length_41 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_41 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } case 3 : { /* increment_char */ unsigned int _camkes_length_42 = increment_char_internal ( ) ; typedef char _assertion_failed__static_assert_23 [ ( ( _camkes_length_42 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_42 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } case 4 : { /* increment_parameter */ unsigned int _camkes_length_43 = increment_parameter_internal ( ) ; typedef char _assertion_failed__static_assert_24 [ ( ( _camkes_length_43 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_43 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } case 5 : { /* increment_64 */ unsigned int _camkes_length_44 = increment_64_internal ( ) ; typedef char _assertion_failed__static_assert_25 [ ( ( _camkes_length_44 <= 120 ) ) ? 1 : - 1 ] __attribute__ ( ( __unused__ ) ) ; /* Send the response */ _camkes_info_36 = seL4_MessageInfo_new ( 0 , 0 , 0 , _camkes_length_44 ) ; seL4_ReplyWait ( 6 , _camkes_info_36 , ( ( void * ) 0 ) ) ; break ; } default : { ( ( void ) 0 ) ; } } return _camkes_info_36 ; }