From 459b7661aaa0d65d01be064bd4b9976c4f045a5c Mon Sep 17 00:00:00 2001 From: zinc Date: Wed, 14 Oct 2026 18:22:04 +0330 Subject: bounds: body scan, loop-entry hoisting, pointer proofs from requested size, --explain-checks v1 (non-o3 code) --- tests/programs/bounds_body.zc | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/programs/bounds_body.zc (limited to 'tests/programs/bounds_body.zc') 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; +} -- cgit v1.2.3