bounds: body scan, loop-entry hoisting, pointer proofs from requested size, --explain-checks v1 (non-o3 code)

1 files changed, 11 insertions, 0 deletions

diff --git a/tests/programs/bounds_body.zc b/tests/programs/bounds_body.zc
new file mode 100644
index 0000000..ea838ac
--- /dev/null
+++ b/tests/programs/bounds_body.zc
@@ -0,0 +1,11 @@
+namespace;
+include rt;
+
+// a loop proof only holds while the body leaves the index alone: here the body
+// moves i back below 0 once, so t[i] keeps its check and the access faults
+int main() {
+	int[4] t; int s = 0, once = 1;
+	for (int i = 0; i < 4; i++) { s = s + t[i]; if (once) { once = 0; i = -3000; } }
+	rt.put_n(s); rt.put_c(10);
+	return 0;
+}