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

Отказ компилятора на стороне flang — значение, поэтому «программа отвергнута» проверяется обычным примером

Считалось, что утверждения вида «такую программу компилятор отвергает таким-то кодом» выразить внутри языка нельзя: flang test гоняет примеры, а отвергнутая программа примеров не запускает вовсе. Отсюда следовал вывод, что такие проверки требуют отдельного обходчика поверх flang check.

Вывод неверен. Слои на flang — обычные функции: «Проверить типы» и «Проверить тотальность» возвращают запись со списком диагностик, у каждой поля «код», «сообщение», «строка», «столбец». Отказ приезжает значением, а не броском, и значение видит обычный пример.

Цепочка складывается прямо в языке:

модуль «Отказы завершаемости» использует «Парсер flang» из "parser.flang" использует «Тотальность flang» из "totality.flang"

функция «Код отказа тотальности» принимает «исходник»: строка возвращает строка пример «Растущий аргумент отвергается» дано «исходник» равно "…«До нуля» от (н плюс 1)…" ожидается "FLANG_NOT_TOTAL" …

Чем подтверждено. Ветка vypusk/zamestit-proverki, коммит d9d68c7f. Файлы flang/self/otkazy-totalnosti.flang и flang/self/otkazy-tipov.flang, девять примеров. Прогон и свидетелем на Node, и двоичным из bootstrap/: 234 из 234 и 202 из 202 — зелено на обоих.

Снял правило и посмотрел, что покраснеет — дважды:

Положительные примеры («та же программа с убыванием на один доказывается») обязательны: без них проверка зеленела бы и у слоя, который отвергает всё подряд.

Две мели, на которые садишься сразу.

  1. использует «Модуль» из "путь" только «Имя», … для эталона не годится: список только режет и внутренние помощники ввезённого слоя, после чего его собственное тело не собирается («неизвестная функция»). Ввозить надо целиком.
  2. Два тяжёлых слоя в один модуль не ввозятся: types.flang и totality.flang берут из emit-c.flang РАЗНЫЕ наборы имён, и связывание обоих сразу оставляет второму неполный список. Поэтому файла два, а не один.

Чем ограничено. Так выражается всё, что решает сам слой на flang. Не выражается то, что решает не он: код возврата процесса, разделение stdout и stderr, файловая система, предел шагов вычислителя, сборка компилятором C, скорость. Для этого обходчик поверх команды по-прежнему нужен.

Связано: flang-test-is-always-green-on-a-layer-with-no-examples-of-its-own, two-language-rules-live-only-in-the-javascript-implementation