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