1/*
2 * Copyright 2016, Data61
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11
12int a_global;
13int a_mod_global;
14int b_mod_global;
15int c_mod_global;
16int d_mod_global;
17
18int
19f (int x) {
20    unsigned int tmp1 = 0;
21    __asm__ volatile("ubfx" "%0, %1, #11, #8" : "=r"(tmp1) : "r"(x));
22    return tmp1;
23}
24
25static inline void do_dmb(void)
26{
27    __asm__ volatile("dmb" "sy" : : : "memory");
28}
29
30int
31g (void) {
32  a_mod_global ++;
33  b_mod_global ++;
34  c_mod_global ++;
35  d_mod_global ++;
36}
37
38/** MODIFIES: [*] */
39void unspecified_function(unsigned int x);
40
41int
42combine (int x) {
43  x = f (x);
44  b_mod_global ++;
45  unspecified_function (x);
46  do_dmb ();
47  g ();
48  x = f (x);
49  return x;
50}
51
52
53
54