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;