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