blob: a678fb32cc801483b74763e6410093c3db0e3de9 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
namespace;
include rt;
// a loop test i < K with a constant K proves the index of a fixed array of at
// least K elements, so the bounds check is dropped: the checked loop compiles
// to exactly as many words as the unbounded one. a variable bound proves
// nothing and keeps the check. sizes come from the functions' line blocks.
int[8] t;
int konst() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
unbounded int bare() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
int vary(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }
unbounded int vbare(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }
int size(word f) { word b = rt.line_block_of(f); return b[2] - b[1]; }
int main() {
rt.put_n(konst() + bare() + vary(8) + vbare(8)); rt.put_c(10);
rt.put_n(size(konst) == size(bare)); rt.put_c(10);
rt.put_n(size(vary) > size(vbare)); rt.put_c(10);
return 0;
}
|
