flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Поле записи отмывало значение из-за симметричного сравнения типов

Что было. В flang/src/types.mjs поле записи сверялось через sameType — симметричное равенство формы, для которого нат, целое и число один и тот же double. Поле варианта рядом сверялось через годится. Список из десяти мест, переведённых на годится, назвал поле варианта и пропустил поле записи.

Измеренное следствие. запись «Ящик» с вес равным (0 минус 1) при вес: нат даёт ноль диагностик. Хуже — поле отмывает значение: выражение «Прямо» от ((запись «Ящик» с вес равным (0 минус 1)).вес) типизируется, хотя «Прямо» принимает нат.

Почему это опасно вдвойне. Тем самым пробивается факт, который у ядра уже есть: ведомость говорит «доказано по объявленным типам аргументов, обо ВСЕХ входах», а прогон той же программы отказывает FLANG_PROPERTY. Прочитай ядро тип поля фактом — оно доказывало бы ложь вторым способом.

Цена починки измерена и не нулевая: правка одного слова ломает flang/self/monoid.flang, где «номер»: нат принимает («сбор».«номер») плюс 1.

Заведена исполняемая улика, краснеющая в обратную сторону — то есть дыра не протухнет молча.

Связано: the-core-proved-a-falsehood, checks-that-stopped-comparing