Отметка слоя типов в дерево не выезжает, поэтому места проверок можно посчитать только внутри компилятора — снаружи выйдет верхняя оценка на 56 % больше

Главное число проекта — сколько функций, обещавших завершение, во время работы не проверяют ничего, — считается по местам частичных форм: элемент, голова, хвост, к числу и ещё четыре формы, определённые не на всех значениях своего типа. На каждое такое место генератор кода ставит проверку.

Но не на каждое. Там, где слой вывода типов доказал непустоту списка или строки, проверки в готовом коде нет вовсе, и место отмечается словом доказана. Отметку кладёт «Отметить доказанные» (flang/self/types.flang) уже после разбора, и в дерево, которое отдаёт команда flang ast, она не выезжает: ast о типах не судит намеренно. Значит, посчитать эти места снаружи — по дереву — нельзя: получится не число, а оценка сверху, выданная за точную.

Чем подтверждено, числом. 244 файла дерева, у которых печатается ведомость доказательства. Счёт внутри компилятора, по отмеченной программе: 401 место у 252 функций. Счёт снаружи, по неотмеченному дереву flang ast, тем же списком из восьми форм и тем же обходом: 626 мест у 363 функций. Разница — 225 мест и 111 функций, то есть внешний счёт завысил бы на 56 %, и до ста одиннадцати функций попали бы в «проверяет» без единой проверки. Ветка vypusk/mesta-proverok, коммиты 8f6ebadf, 4c071a5b, 1aa34714.

Поштучно то же самое видно на четырёх строках:

длина «числа»                                    → 0 мест
если пусто «числа» то 0 иначе голова «числа»     → 0 мест (непустота доказана)
голова «числа»                                   → 1 место
(элемент 1 в «числа») плюс (элемент 2 в «числа») → 2 места

Первая и третья различаются только отметкой: форма одна и та же.

Чем ограничено. Утверждение про одну отметку — доказана. Вторая отметка того же рода (числовая, снимающая сверку типов у двуместной операции) здесь не мерена. И число 626 получено обходом, который знает только вид узла и список из восьми имён; обход внутри компилятора тот же самый, так что разница — целиком отметка, а не разные правила счёта.

Отсюда правило. Всё, что решает слой типов, снаружи не воспроизводимо в принципе, а не «пока не написано». Инструмент, которому нужен такой ответ, обязан спрашивать компилятор, а не разбирать дерево заново.

Связано: vedomost-dvoichnogo-byvaet-slabee-i-nikogda-ne-silnee, a-number-with-no-key-drifts-from-its-own-report, an-unlinked-module-collects-names-that-are-already-taken