prover: do not restore length facts after a call-loop

Restoring undirtied lafacts when the body might free was wrong: push can
grow an array without dirtying its name, so a[99] after push warned against
a stale length 0. Keep the old lafact_keep rule; reorder explain_prover so
the constant/affine cases run before the touch() loops.

1 files changed, 5 insertions, 3 deletions

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;