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