1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7
8int a_global;
9int a_mod_global;
10int b_mod_global;
11int c_mod_global;
12int d_mod_global;
13
14int
15f (int x) {
16    unsigned int tmp1 = 0;
17    __asm__ volatile("ubfx" "%0, %1, #11, #8" : "=r"(tmp1) : "r"(x));
18    return tmp1;
19}
20
21static inline void do_dmb(void)
22{
23    __asm__ volatile("dmb" "sy" : : : "memory");
24}
25
26int
27g (void) {
28  a_mod_global ++;
29  b_mod_global ++;
30  c_mod_global ++;
31  d_mod_global ++;
32}
33
34/** MODIFIES: [*] */
35void unspecified_function(unsigned int x);
36
37int
38combine (int x) {
39  x = f (x);
40  b_mod_global ++;
41  unspecified_function (x);
42  do_dmb ();
43  g ();
44  x = f (x);
45  return x;
46}
47
48
49
50