Files
scriptc/tests
Chris Tate 723975d01c Prove that the arrays InlineArray fields hold are never written
The constructor copies the array it is passed into the instance, and
other reads of the field give a new array over the elements, while under
Node.js the field holds that array itself. The contract check now proves
the two agree, and reports SC7009 where it cannot:

- The arrays fields hold are never written. A whole-program graph of the
  places arrays are held (locals, parameters, results, class and record
  fields, and the elements of arrays, Maps and Sets by where those are
  held) follows every array a field read may give, and reports a write to
  one, or one that reaches a dynamic value, a call through a function
  value or a library call other than printing and JSON.stringify without
  a replacer. Functions that return their argument give each caller its
  own argument back. The report names the field read.
- The array passed to the constructor is one nothing else keeps: a new
  array (a literal, a copy, or the result of a function that returns only
  such arrays or its argument), a local array at its last use (after calls
  that only read it or write it in place, or in a loop that then assigns
  the local a new array), a parameter whose every caller passes such an
  array, an array a field already holds, or a const array that is never
  written, which is then followed like a field's.

The review fixes from before stay: `new` evaluates its arguments into
locals unless they are all locals and constants, so that the allocation
reads the length after every argument has run; the constructor uses the
array parameter only to store it; and the dynamic view of an instance
reads the field as an array of its elements.
2026-10-27 02:38:15 -05:00
..
2026-10-26 10:20:11 -05:00
2026-10-26 06:51:26 -05:00
…