diff options
| author | 2026-10-14 16:09:07 +0330 | |
|---|---|---|
| committer | 2026-10-14 16:09:07 +0330 | |
| commit | e228e7609929763d5acddb728ba543832fcffc6a (patch) | |
| tree | 9b4ecc4d46bf38e8d20234d631a6d41543daa211 /tests/programs/boundsrules.zc | |
| parent | merge: memdebug obj_base via size classes (diff) | |
| parent | bounds 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.zc | 24 |
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; +} |
