1/*
2 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#include <assert.h>
8#include <camkes.h>
9#include <sel4/sel4.h>
10#include <stdbool.h>
11#include <stdio.h>
12
13void f_foo(void) {
14    static seL4_Word badge;
15    static bool not_first;
16    if (!not_first) {
17        badge = f_get_sender_id();
18        not_first = true;
19    } else {
20        seL4_Word new_badge = f_get_sender_id();
21        assert(new_badge != badge);
22        if (new_badge != badge) {
23            printf("All OK\n");
24        }
25    }
26}
27