aboutsummaryrefslogtreecommitdiff
path: root/tests/programs/boundsrules.zc
diff options
context:
space:
mode:
authorGravatar zinc <zinc@downsta.ir> 2026-10-14 16:09:07 +0330
committerGravatar zinc <zinc@downsta.ir> 2026-10-14 16:09:07 +0330
commite228e7609929763d5acddb728ba543832fcffc6a (patch)
tree9b4ecc4d46bf38e8d20234d631a6d41543daa211 /tests/programs/boundsrules.zc
parentmerge: memdebug obj_base via size classes (diff)
parentbounds checking: constant loop bound proof works, plain-op fixed-array check,... (diff)
merge bounds checking
Diffstat (limited to 'tests/programs/boundsrules.zc')
-rw-r--r--tests/programs/boundsrules.zc24
1 files changed, 24 insertions, 0 deletions
diff --git a/tests/programs/boundsrules.zc b/tests/programs/boundsrules.zc
new file mode 100644
index 0000000..1ae6a56
--- /dev/null
+++ b/tests/programs/boundsrules.zc
@@ -0,0 +1,24 @@
+namespace;
+include rt;
+
+// unbounded turns the checks off: as a function prefix (in any order with
+// unchecked), as a block, for one statement. o3 implies it. the last read is
+// checked and stops the program.
+int[8] pad;
+int[4] a;
+
+unbounded int pre(int i) { return a[i] * 0 + 1; }
+unchecked unbounded int both(int i) { return a[i] * 0 + 1; }
+o3 int fast(int i) { return a[i] * 0 + 1; }
+int blk(int i) { int r = 0; unbounded { r = a[i] * 0 + 1; } return r; }
+int one(int i) { int r = 0; unbounded r = a[i] * 0 + 1; return r; }
+int checked(int i) { return a[i]; }
+
+int main() {
+ int i = 5;
+ a[3] = 7;
+ rt.put_n(pre(i) + both(i) + fast(i) + blk(i) + one(i)); rt.put_c(10);
+ rt.put_n(checked(3)); rt.put_c(10);
+ rt.put_n(checked(i)); rt.put_c(10);
+ return 0;
+}