Сторона на flang для анализа завершаемости не читает обеспечивает, и это тот же баг, который свидетель у себя уже чинил

flang/src/totality.mjs считает вызовы из постусловия частью вызова функции: тотальная функция, чьё обеспечивает зовёт обычную или неизвестную, — не тотальная. В шапке свидетеля это записано как ПОЧИНЕННАЯ ошибка: «поле postconditions анализ не читал вовсе, и такая функция проходила flang check молча». В flang/self/totality.flang эта ошибка всё ещё открыта — поле postconditions там не упоминается ни разу.

Дыра не всплывала два месяца, потому что для неё нужно редкое совпадение: у функции ТЕЛО должно обходиться без ввезённых имён, а ПОСТУСЛОВИЕ — звать ввезённое. Тогда на неразобранной (несвязанной) программе свидетель говорит «нетотальна», а сторона на flang — «тотальна», и два анализа расходятся.

Чем подтверждено. Проверка flang/test/self-totality.test.mjs, «каждая программа репозитория без связывания получает тот же вердикт», на ветке work/goryachaya-zamena: flang/self/hotswap.flang: множество тотальных разошлось: лишние ["Ответ отказа"], недостающие []. «Ответ отказа» — единственная функция того файла, чьё тело зовёт только местные имена (вызов без аргументов, («Узел ничто»), за вызов не считается ни тем, ни другим анализом). Когда множества свели, разошлись ДИАГНОСТИКИ: свидетель печатает «зовёт неизвестную функцию „Есть поле у узла“ в постусловии», сторона на flang — молчит. Обход: постусловия переписаны так, чтобы звать только местные имена; одно постусловие, которому для этого не хватило местных имён, снято, а его утверждение проверяет побайтовая сверка на 4918 случаях.

Чем ограничено. Это НЕ про связанные программы: после связывания все имена известны, и оба анализа сходятся — дыра видна только на «сыром» вердикте. Поэтому она и не красит ни flang check, ни собственные проверки файла: её ловит один сторож всего дерева, и только на файле нужной формы.

Чему учит. Заводя постусловие в flang/self/*.flang, зовите из него только имена, объявленные в том же файле, — пока дыра не закрыта. И проверяйте новый файл flang/self/ сторожем всего дерева, а не только его собственной сверкой: именно на этом сторже откатили прошлую попытку горячей замены (5a7a460b, 497 строк, исчерпание 280 000 000 шагов) — её собственные проверки были зелены.

Дополнение, 20 августа: дыра измерена НАПРЯМУЮ, а не через расхождение множеств. Цепочка «Разбор исходника» → «Проверить тотальность» собрана файлом flang/self/otkazy-totalnosti.flang и позволяет спросить эталон о любом исходнике. На программе

функция «Вечная» … «Вечная» от н тотальная функция «Ф» для всех н обеспечивает «всегда» «Вечная» от н н

свидетель отвечает FLANG_NOT_TOTAL и называет обе функции, эталон — пустой строкой, то есть отказов нет. Дыра, значит, не только на «сыром» вердикте: она видна и на связанной программе, если постусловие зовёт функцию, объявленную рядом. Держит это правило ровно один тест дерева — flang/test/totality.test.mjs «постусловие — тоже код: вызов обычной функции из него отвергается», и он на JavaScript.

Это оказался не единичный случай, а класс: a-rule-no-corpus-program-touches-is-invisible-to-the-reference-check.

Связано: a-rule-no-corpus-program-touches-is-invisible-to-the-reference-check, a-red-inherited-from-the-trunk-must-be-measured-on-the-trunk, handler-postcondition-escapes-the-closed-set, four-pieces-of-javascript