Header files for the ARM7 example program

Header file count_t.h

 1  #if !defined(COUNT_T)
 2  #define COUNT_T
 3  
 4  typedef int count_t;
 5  
 6  #endif

Header file types.h

 1  #if !defined(TYPES)
 2  #define TYPES
 3  
 4  typedef unsigned int uint;
 5  
 6  typedef unsigned char uchar;
 7  
 8  #include "count_t.h"
 9  
10  #endif

Header file routines.h

 1  #include "types.h"
 2  
 3  extern void Count25 (uint *x);
 4  /* Demonstrates a loop with static bounds. */
 5  
 6  extern void Count (count_t u, uint *x);
 7  /* Demonstrates a loop that depends on the parameter u. */
 8  
 9  extern void Foo (count_t num, uint *x);
10  /* Demonstrates a call to Count that makes Count.u depend on */
11  /* Foo.num, so that the loop in Count depends on Foo.num.    */
12  
13  extern void Foo7 (uint *x);
14  /* Demonstrates a call to Foo with a static value for Foo.num  */
15  /* which passes on to Count.u and lets Bounds-T bound the loop */
16  /* in Count.                                                   */
17  
18  extern void Solve (uint *x);
19  /* Demonstrates a for-loop with static bounds.               */
20  /* Demonstrates bounding a call (on Count) using assertions. */
21  
22  extern count_t Ones (uint x);
23  /* Returns the number of '1' bits in x.                      */
24  /* Demonstrates a 'while' loop for which Bound-T cannot find */
25  /* a loop-bound automatically.                               */