1/* 2 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#include <camkes.h> 8#include <stdio.h> 9#include <string.h> 10#include <sel4/sel4.h> 11 12int run(void) { 13 const char *shello = "hello world"; 14 15 printf("Starting...\n"); 16 printf("-----------\n"); 17 18 strcpy((void*)DataOut, shello); 19 while(!*((char*)DataIn)) 20 seL4_Yield(); 21 printf("%s read %s\n", get_instance_name(), (char*)DataIn); 22 return 0; 23} 24