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. */