Header files for the Atmel AVR example program

Header file count_t.h


 1  /*
 2  
 3  A part of the Bound-T test program tp_bro_int.
 4  This is the example program in the Bound-T brochure.
 5  This version uses "int" counters.
 6  
 7  $Id: headers.html,v 1.1 2010-02-27 09:52:18 niklas Exp $
 8  */
 9  
10  
11  #if !defined(COUNT_T)
12  #define COUNT_T
13  
14  typedef int count_t;
15  
16  #endif

Header file types.h


 1  /*
 2  
 3  A part of the Bound-T test program tp_bro_int.
 4  This is the example program in the Bound-T brochure.
 5  
 6  $Id: headers.html,v 1.1 2010-02-27 09:52:18 niklas Exp $
 7  */
 8  
 9  
10  #if !defined(TYPES)
11  #define TYPES
12  
13  typedef unsigned int uint;
14  
15  typedef unsigned char uchar;
16  
17  #include "count_t.h"
18  
19  #endif

Header file routines.h


 1  /*
 2  
 3  A part of the Bound-T test program tp_bro_int.
 4  This is the example program in the Bound-T brochure.
 5  
 6  $Id: headers.html,v 1.1 2010-02-27 09:52:18 niklas Exp $
 7  */
 8  
 9  
10  #include "types.h"
11  
12  extern void Count25 (uint *x);
13  /* Demonstrates a loop with static bounds. */
14  
15  extern void Count (count_t u, uint *x);
16  /* Demonstrates a loop that depends on the parameter u. */
17  
18  extern void Foo (count_t num, uint *x);
19  /* Demonstrates a call to Count that makes Count.u depend on */
20  /* Foo.num, so that the loop in Count depends on Foo.num.    */
21  
22  extern void Foo7 (uint *x);
23  /* Demonstrates a call to Foo with a static value for Foo.num  */
24  /* which passes on to Count.u and lets Bounds-T bound the loop */
25  /* in Count.                                                   */
26  
27  extern void Solve (uint *x);
28  /* Demonstrates a for-loop with static bounds.               */
29  /* Demonstrates bounding a call (on Count) using assertions. */
30  
31  extern count_t Ones (uint x);
32  /* Returns the number of '1' bits in x.                      */
33  /* Demonstrates a 'while' loop for which Bound-T cannot find */
34  /* a loop-bound automatically.                               */