diff options
| author |  zinc <zinc@downsta.ir>
| 2026-10-15 05:23:36 +0330 |
|---|---|---|
| committer | zinc <zinc@downsta.ir>
| 2026-10-15 05:23:36 +0330 |
| commit | fe43cc41876ffdb3e714de8efc8a2907d456b5db (patch) | |
| tree | acb86b8b5c46a6ce77a43d3be3a6aa9c8a41abb6 /tests/programs/bounds_prover.expected | |
| parent | wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, aff... (diff) | |
prover: len/cross-array/fixed-new/affine proofs; keep facts past call loops
Rebased the prover WIP onto main. lafact_keep restores undirtied allocation
facts even when the loop body might free (so a later touch() no longer drops
every length fact). proven_p uses ptr_still so an outer call keeps the check.
entry_fact still supplies the size for the "might free" explain reason.
bounds_prover.zc and explain_prover.zc land with test.sh coverage.
Diffstat (limited to 'tests/programs/bounds_prover.expected')
| -rw-r--r-- | tests/programs/bounds_prover.expected | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/programs/bounds_prover.expected b/tests/programs/bounds_prover.expected new file mode 100644 index 0000000..f5e92fa --- /dev/null +++ b/tests/programs/bounds_prover.expected @@ -0,0 +1,4 @@ +28 +36 +0 1 2 3 4 5 6 zy: index 6 out of range (length 6) + at <stdin>:17 in main |