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 f(int x)
15{
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 g(void)
27{
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 combine(int x)
38{
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