diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/programs/bounds_proof.zc | 21 | ||||
| -rwxr-xr-x | tests/test.sh | 1 |
2 files changed, 22 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; +} diff --git a/tests/test.sh b/tests/test.sh index 7a80c3c..1625680 100755 --- a/tests/test.sh +++ b/tests/test.sh @@ -227,6 +227,7 @@ ABC" "$l o3 lifts byte loads and stores" chk "$($vm < tests/programs/boundsrules.zc 2>&1 | head -3)" $'5\n7\nzy: index 5 out of range (length 4)' "$l unbounded as prefix, block and statement, o3 implies it; checked code reports" chk "$($vm < tests/programs/bounds_fixed.zc 2>&1 | head -3)" $'55\n29\nzy: index 6 out of range (length 6)' "$l a fixed array with a variable index is checked against its length" chk "$($vm < tests/programs/bounds_heap.zc 2>&1 | head -4)" $'3\n0\nx\nzy: index 11 out of range (length 11)' "$l a pointer to a heap block is checked against its payload" + chk "$($vm < tests/programs/bounds_proof.zc)" $'0\n1\n1' "$l a loop test against a constant drops the fixed-array check; a variable bound keeps it" chk "$($vm < tests/programs/zc0unbounded.zc)" "42" "$l unbounded in the unit, a prefix and a statement" local r; r=$(bash tests/runerr.sh "$vm" tests/errors | tail -1) chk "$r" "rejected: $(ls tests/errors/*.zc | wc -l | tr -d ' ') passed, 0 failed" "$l analyzer rejects every bad program" |