SPARC/ERC32 example: source file exa.adb
1 -- Example Ada/ERC32 program for Bound-T.
2 -- Copyright (c) 2006 Tidorum Ltd.
3
4
5 procedure Exa is
6
7 type Unsigned_Int is mod 2**32;
8
9
10 function Ones (X : Unsigned_Int) return Natural
11 --
12 -- Returns the number of '1' bits in X.
13 -- Demonstrates a "while" loop for which Bound-T cannot find
14 -- the number of iterations automatically.
15 --
16 is
17
18 V : Natural := 0;
19 -- The number of '1' bits seen so far.
20
21 R : Unsigned_Int := X;
22 -- The part of X not yet examined.
23
24 begin
25
26 while R /= 0 loop
27
28 if (R and 1) /= 0 then
29 V := V + 1;
30 end if;
31
32 R := R / 2;
33
34 end loop;
35
36 return V;
37
38 end Ones;
39
40
41 procedure Count25 (X : access Unsigned_Int)
42 --
43 -- Demonstrates a loop with static bounds, but a little
44 -- more complex than a "for" loop.
45 --
46 is
47 U : Integer := 25;
48 -- The counter.
49 begin
50
51 while U > 0 loop
52
53 X.all := X.all * Unsigned_Int(U);
54
55 U := U - 2;
56
57 end loop;
58
59 end Count25;
60
61
62 procedure Count (
63 U : in Integer;
64 X : access Unsigned_Int)
65 --
66 -- Demonstrates a loop that depends on a parameter (U).
67 --
68 is
69 W : Integer := U;
70 -- A local counter for the loop.
71 begin
72
73 while W > 0 loop
74
75 X.all := X.all * Unsigned_Int(U);
76
77 W := W - 2;
78
79 end loop;
80
81 end Count;
82
83
84 procedure Foo7 (X : access Unsigned_Int) is
85 --
86 -- Demonstrates a call to Count with a static value of Count.U
87 -- that lets Bound-T bound the loop in Count.
88 --
89 begin
90
91 X.all := X.all + 10;
92
93 Count (7, X);
94 -- The loop in Count depends on Count.U = 7.
95
96 X.all := X.all - 8;
97
98 end Foo7;
99
100
101 procedure Foo (
102 Num : in Integer;
103 X : access Unsigned_Int) is
104 --
105 -- Demonstrates a call to Count that makes Count.U depend on
106 -- Foo.Num, so that the loop in Count depends on Foo.Num.
107 --
108 begin
109
110 Count (Num + 3, X);
111
112 end Foo;
113
114
115 procedure Solve (X : access Unsigned_Int)
116 --
117 -- Demonstrates a "for"-loop with static bounds.
118 -- Demonstrates bounding a call (on Count) with assertions.
119 --
120 is
121 K : Integer;
122 pragma Volatile (K);
123 -- To make sure that K is mapped to a storage location.
124 begin
125
126 for I in 0 .. 7 loop
127 -- The bounds (0..7) in this loop are static.
128
129 K := Ones (X.all);
130 -- K is now the number of '1' bits in X.all.
131 -- This would be quite hard to analyse statically.
132
133 exit when K = 0;
134
135 Count (U => K, X => X);
136
137 end loop;
138
139 end Solve;
140
141
142 procedure Main
143 --
144 -- Demonstrates calls of various routines.
145 --
146 is
147
148 X : aliased Unsigned_Int;
149 -- A working variable. Bound-T will not be able to track
150 -- the value of this variable because it is changed in
151 -- the called routines.
152
153 begin
154
155 Count25 (X'access);
156 -- This can be bounded automatically because the loop
157 -- in Count25 has static bounds.
158
159 Foo7 (X'access);
160 -- This can be bounded automatically because Foo7 calls
161 -- Count with a static value for Count.U.
162
163 Foo (Num => 6, X => X'access);
164 -- This can be bounded automatically because Foo.Num = 6,
165 -- which makes Count.U = 9, which bounds the loop in Count.
166
167 Solve (X => X'access);
168 -- The loop in Solve can be bounded automatically, but
169 -- not the loop in Count when called from Solve.
170
171 loop
172 null;
173 end loop;
174 -- This is a simple eternal loop. Bound-T will report it
175 -- and the number of iterations to be included in the WCET
176 -- must be asserted.
177
178 end Main;
179
180
181 begin
182
183 Main;
184
185 end Exa;