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