1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7procedure s {
8    int echo_int(in int i);
9    int echo_parameter(in int pin, out int pout);
10    int echo_char(in char i);
11    void increment_char(inout char x);
12    void increment_parameter(inout int x);
13    void increment_64(inout uint64_t x);
14}
15