diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/programs/explain_prover.expected | 16 | ||||
| -rw-r--r-- | tests/programs/explain_prover.zc | 8 |
2 files changed, 13 insertions, 11 deletions
diff --git a/tests/programs/explain_prover.expected b/tests/programs/explain_prover.expected index c43c72d..f6854c7 100644 --- a/tests/programs/explain_prover.expected +++ b/tests/programs/explain_prover.expected @@ -1,9 +1,9 @@ {"version":1} -{"file":"<eval>","line":18,"col":42,"end_line":18,"end_col":45,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"} -{"file":"<eval>","line":22,"col":51,"end_line":22,"end_col":54,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} -{"file":"<eval>","line":26,"col":62,"end_line":26,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"} -{"file":"<eval>","line":27,"col":71,"end_line":27,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} -{"file":"<eval>","line":30,"col":46,"end_line":30,"end_col":49,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} -{"file":"<eval>","line":34,"col":81,"end_line":34,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} -{"file":"<eval>","line":35,"col":70,"end_line":35,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} -{"file":"<eval>","line":36,"col":59,"end_line":36,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} +{"file":"<eval>","line":19,"col":42,"end_line":19,"end_col":45,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"} +{"file":"<eval>","line":23,"col":51,"end_line":23,"end_col":54,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} +{"file":"<eval>","line":29,"col":46,"end_line":29,"end_col":49,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} +{"file":"<eval>","line":33,"col":81,"end_line":33,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} +{"file":"<eval>","line":34,"col":70,"end_line":34,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} +{"file":"<eval>","line":35,"col":59,"end_line":35,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"} +{"file":"<eval>","line":37,"col":62,"end_line":37,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"} +{"file":"<eval>","line":38,"col":71,"end_line":38,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"size-unknown","fix":"the compiler does not know the size of the block; allocate it here with a constant size, or index a fixed array"} diff --git a/tests/programs/explain_prover.zc b/tests/programs/explain_prover.zc index 14486b5..088cb1d 100644 --- a/tests/programs/explain_prover.zc +++ b/tests/programs/explain_prover.zc @@ -3,6 +3,7 @@ include rt; // the loop prover, case by case: each "kept" line must stay in zy --explain-checks // and each "proved" line must not. run, it prints one checksum. +// call-loops come last: they clear allocation facts for the rest of the function. int touch() { return 0; } int[16] sq; int main() { @@ -20,11 +21,9 @@ int main() { for (i = 0; i < len(a); i++) s = s + b[i]; // proved: 8 <= 10 for (i = 0; i < len(a); i++) s = s + sq[i]; // proved: 8 <= 16 for (i = 0; i < len(a); i++) if (i < 6) s = s + c[i]; // kept: 6 < 8 - // 3. a pointer of constant size at depth 2 and 3 + // 3. a pointer of constant size for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) p[j] = j; // proved for (i = 0; i < 2; i++) for (k = 0; k < 2; k++) for (j = 0; j < 16; j++) s = s + p[j]; // proved - for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) { s = s + p[j]; touch(); } // kept: the body calls - for (i = 0; i < 2; i++) { touch(); for (j = 0; j < 16; j++) s = s + p[j]; } // kept: the outer body calls // 4. new(fixed int[?], n) with a constant n for (i = 0; i < 6; i++) s = s + c[i]; // proved for (i = 0; i < 7; i++) if (i < 6) s = s + c[i]; // kept: 7 > 6 @@ -34,6 +33,9 @@ int main() { for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) if (i * 4 + k < 15) s = s + m15[i * 4 + k]; // kept: 15 < 16 for (i = 0; i < 4; i++) for (k = 0; k < 5; k++) if (k < 4) s = s + m[i * 4 + k]; // kept: k < 5 for (i = 0; i < n; i++) for (k = 0; k < n; k++) s = s + m[i * n + k]; // kept: n is a variable + // 6. a call in the body keeps the check (clears facts afterward) + for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) { s = s + p[j]; touch(); } // kept: the body calls + for (i = 0; i < 2; i++) { touch(); for (j = 0; j < 16; j++) s = s + p[j]; } // kept: the outer body calls rt.put_n(s); rt.put_c(10); rt.free(d*a); rt.free(d*b); rt.free(d*c); rt.free(d*m); rt.free(d*m15); rt.free(p); return 0; |