Merge branch 'main' into work/spec

1 files changed, 21 insertions, 0 deletions

diff --git a/tests/programs/bounds_proof.zc b/tests/programs/bounds_proof.zc
new file mode 100644
index 0000000..a678fb3
--- /dev/null
+++ b/tests/programs/bounds_proof.zc
@@ -0,0 +1,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;
+}