1/*
2 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7import <std_connector.camkes>;
8
9procedure P {
10    int echo(in int x);
11}
12
13component Foo {
14    control;
15    uses P outgoing;
16    provides P incoming;
17}
18
19component Bar {
20    provides P incoming;
21    uses P outgoing;
22}
23
24assembly {
25    composition {
26        component Foo foo;
27        component Bar bar;
28
29        connection seL4RPCCall conn1(from foo.outgoing, to bar.incoming);
30        connection seL4RPCCall conn2(from bar.outgoing, to foo.incoming);
31    }
32}
33