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, 8 insertions, 8 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"}