1/* 2 * Copyright 2014, NICTA 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 11unsigned global; 12 13int mult(int x, int y) 14{ 15 return x * y; 16} 17 18int fact(int n) 19{ 20 int factor, total; 21 total = 1; 22 factor = 2; 23 while (factor <= n) 24 /** INV: "\<lbrace> unat \<acute>total = fac (unat \<acute>factor - 1) & 25 \<acute>factor \<le> \<acute>n + 1 26 \<rbrace>" */ 27 { 28 total = mult(factor, total); 29 factor = factor + 1; 30 } 31 return total; 32} 33 34/** FNSPEC 35 g_modifies: "\<forall> \<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC g() {t. t may_not_modify_globals \<sigma>}" 36*/ 37int g(void) 38{ 39 return 257; 40} 41 42/** FNSPEC 43 f_spec: "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== PROC f(n) \<lbrace> \<acute>ret__int = 1 \<rbrace>" 44 f_modifies: "\<forall>\<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC f(\<acute>n) 45 {t. t may_not_modify_globals \<sigma>}" 46*/ 47int f (int n) 48{ 49 char c; 50 global++; 51 c = g(); 52 return c; 53} 54 55 56/** FNSPEC 57 h_modifies: 58 "\<forall> \<sigma>. 59 \<Gamma> \<turnstile> 60 {\<sigma>} 61 \<acute>ret__ptr_to_void :== PROC h() 62 {t. t may_not_modify_globals \<sigma>}" 63*/ 64void *h(void) 65{ 66 return 0; 67} 68 69/** FNSPEC 70 i_modifies: "\<forall> \<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC i() {t. t may_not_modify_globals \<sigma>}" 71*/ 72int i(void) 73{ 74 int *iptr = h(); 75 return iptr[3]; 76} 77 78/** FNSPEC 79 has_bogus_spec_spec: "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== PROC has_bogus_spec() \<lbrace> \<acute>ret__int = 4 \<rbrace>" 80*/ 81int has_bogus_spec(void) 82{ 83 return 3; 84} 85 86int calls_bogus(void) 87{ 88 return has_bogus_spec(); 89} 90