Reading compiler errors

A compiler message is not an obstacle but the result of a check you ordered yourself. The compiler does not guess your intent: it names the code, the place and the mismatch. All that is left is translating from the language of the diagnostic into the language of the model.

Each diagnostic below is shown the way flang 0.7.29 prints it: a small program, the output word for word, and the fix. Every program in this chapter is wrong on purpose — paste any of them into the sandbox and you get the same answer.

How a diagnostic is built

A finding is one line:

FLANG_TYPE в файле name1.flang, строка 9, столбец 15: запись «Покупка» не имеет поля «стоимость»

First the code (FLANG_TYPE), then the place, then the text. The code is stable and meant for programs: editor and CI handlers are written against it. The text is meant for people. Almost everything has a place; a failed example does not — it belongs to a function call, not to a line of the file.

flang check collects all findings in one run and ends with a summary line:

type2.flang: не проверено — замечаний 2

One cause often produces a chain of two or three findings. Fix the first one and check again.

The exit code is the main thing CI reads:

Parse errors

Until the text is parsed, no meaning checks happen.

FLANG_PARSE — an если without a то branch. Indentation in flang carries meaning, as in Python, and the то and иначе branches must be named.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  если сумма не меньше 10000
    500
    иначе 0

FLANG_PARSE в файле parse1.flang, строка 7, столбец 5: у 'если' нет ветки 'то'

Fix: то 500.

The same message appears when the condition uses a word the language does not have. Comparisons in flang form a closed list: равен, не равен, больше, меньше, не больше, не меньше.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  если сумма превышает 10000
    то 500
    иначе 0

FLANG_PARSE в файле parse2.flang, строка 6, столбец 14: у 'если' нет ветки 'то'

The message is misleading here: the то branch is in place, but parsing tripped over превышает — column 14 points exactly at that word. Read the column, not only the text. Fix: если сумма больше 10000.

FLANG_UNKNOWN_NAME — an unknown type.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: рубли
  возвращает число
  0

FLANG_UNKNOWN_NAME в файле name3.flang, строка 3, столбец 1: неизвестный тип «рубли»

Fix: a built-in type (число, неотрицательное, строка, признак, сотых for money in kopecks) or your own — тип «Рубли» with variants or объект «Рубли» with fields.

Model errors

The text is parsed, but the program contradicts itself: a name is not found, a type is wrong, a match is incomplete, termination is not proved.

FLANG_TYPE: no such field — the most common error after renaming a field.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«стоимость» не меньше 10000
    то 500
    иначе 0

FLANG_TYPE в файле name1.flang, строка 9, столбец 15: запись «Покупка» не имеет поля «стоимость»

Fix: name the field as it is declared in the object — покупка.«сумма».

FLANG_UNKNOWN_NAME and FLANG_NOT_TOTAL: an unknown function. One cause, two findings: the function does not exist, and so the termination of the one calling it cannot be proved.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  «Надбавка» от сумма

без доказанного завершения: «Скидка»
FLANG_UNKNOWN_NAME в файле name4.flang, строка 6, столбец 3: неизвестная функция «Надбавка»
FLANG_NOT_TOTAL в файле name4.flang, строка 6, столбец 3: тотальная функция «Скидка» вызывает неизвестную функцию «Надбавка»: завершение доказать нельзя

Fix: declare «Надбавка» or correct the name. The second finding goes away on its own.

FLANG_TYPE: the body gives the wrong type. Division gives число even when the dividend is non-negative.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает неотрицательное
  сумма делить на 10

FLANG_TYPE в файле type1.flang, строка 6, столбец 9: функция «Скидка» объявлена как неотрицательное, а тело даёт число

Fix: возвращает число. The type неотрицательное is the integers from 0 to 2⁵³−1, and a quotient does not fit into it.

FLANG_TYPE: an ordering comparison on a string. больше and меньше are defined only for numbers.

модуль «Продажи»

тотальная функция «Скидка»
  принимает клиент: строка
  возвращает число
  если клиент больше 10
    то 500
    иначе 0

FLANG_TYPE в файле type2.flang, строка 6, столбец 8: левый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел
FLANG_TYPE в файле type2.flang, строка 6, столбец 15: сравнение «gt» между строка и неотрицательное

Fix: compare a numeric field, or compare a string with a string using равен.

FLANG_TYPE: a field declared twice.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное
  «сумма»: число

FLANG_TYPE в файле dup1.flang, строка 3, столбец 1: поле «сумма» объявлено дважды

FLANG_MATCH_NOT_EXHAUSTIVE — a разбор did not name every variant of the type. This is the main reason to use a type with variants instead of a string: a forgotten state shows up at check time, not in production.

модуль «Исполнение заказа»

тип «Решение»
  вариант «Разрешено»
  вариант «Отказано» содержит причина: строка

тотальная функция «Словами»
  принимает решение: «Решение»
  возвращает строка
  разбор решение
    случай «Разрешено»
      то "можно отгружать"

FLANG_MATCH_NOT_EXHAUSTIVE в файле match1.flang, строка 10, столбец 3: разбор «Решение» не покрывает «Отказано»

Fix: add случай вариант «Отказано» с причина как причина and an answer for it.

FLANG_NOT_TOTAL — for a function marked тотальная the compiler could not prove termination. Recursion has to move towards a smaller value.

модуль «Остаток»

тотальная функция «Ждать оплаты»
  принимает дней: неотрицательное
  возвращает число
  если дней больше 0
    то «Ждать оплаты» от дней
    иначе 0

FLANG_NOT_TOTAL в файле tot1.flang, строка 7, столбец 8: тотальная функция «Ждать оплаты»: рекурсивный вызов «Ждать оплаты» не убывает — аргумент 1 («дней») — это сам параметр «дней», а не его часть. Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции

Fix: «Ждать оплаты» от (дней минус 1) — the compiler accepts a descent on неотрицательное by exactly one. If the rule does not need recursion, better not to write it at all: walking a list is свёртка or отобразить.

Runtime errors

The program is checked, but a call on a specific input broke a promise or arrived with the wrong type.

flang run requires explicit consent to run a program that failed verification. In this example flang 0.7.32 already finds a violation during flang check.

модуль «Скидка заказа»

тотальная функция «Скидка»
  принимает сумма: неотрицательное, промокод: признак
  возвращает число
  обеспечивает «скидка не больше четверти суммы» результат не больше (сумма делить на 4)
  пример «промокод на крупном заказе»
    дано сумма равно 20000
    дано промокод равно да
    ожидается 500
  если промокод
    то 500
    иначе 0

flang check exits with code 1. The counterexample is an order for 0 with a promo code. A plain flang run stops with code 3 and points to the verification error.

FLANG_PROPERTY — with --trust consent the computation runs, and the promise is checked on the real input:

$ flang run run1.flang --trust --function «Скидка» --args '{"сумма":1000,"промокод":true}'
на веру: доказанность не считалась — запуск по ключу --trust
FLANG_PROPERTY: нарушено свойство «скидка не больше четверти суммы» функции «Скидка»

The same refusal comes from printed code: flang emit puts an unproved promise as a check into every printed function, and a call from JavaScript throws an error with code: "FLANG_PROPERTY" and the same text. The fix is not in the calling code but in the rule: the rule did not foresee a promo code on a one-thousand-rouble order.

FLANG_TYPE: an argument outside its type. flang run arguments are checked against the declared types before computing:

$ flang run run1.flang --trust --function «Скидка» --args '{"сумма":-1000,"промокод":true}'
FLANG_TYPE: вызов функции «Скидка»: аргумент «сумма»: -1000 вне неотрицательное

For an HTTP service this is a client error — 400, not 500.

Example errors

An example is part of a function, and flang check runs it on every check.

FLANG_EXAMPLE — the answer did not match the expectation.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «на двадцать тысяч — две тысячи»
    дано сумма равно 20000
    ожидается 2500
  (сумма умножить на 10) делить на 100

FLANG_EXAMPLE: пример «на двадцать тысяч — две тысячи» функции «Скидка»: значение не совпало с ожидаемым: ожидалось 2500, получено 2000

There are two fixes, and choosing between them is a decision, not mechanics. If the rule is right, the example is wrong: ожидается 2000. If the example is right, the rule has drifted. Adjusting ожидается to the actual answer without asking the rule’s owner means deleting the test.

FLANG_EXAMPLE with FLANG_PROPERTY — an example broke a promise of the same function.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше тысячи» результат не больше 1000
  пример «на двадцать тысяч»
    дано сумма равно 20000
    ожидается 2000
  (сумма умножить на 10) делить на 100

FLANG_EXAMPLE: пример «на двадцать тысяч» функции «Скидка»: FLANG_PROPERTY: нарушено свойство «скидка не больше тысячи» функции «Скидка»

The example and the promise contradict each other, and the compiler does not know which is right. Usually the promise is wrong: the rule has no “at most a thousand” cap.

FLANG_TYPE and FLANG_UNKNOWN_NAME in дано — a typo in an argument name gives two findings: the real argument is not set, and the one set is unknown.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «опечатка в имени аргумента»
    дано сума равно 20000
    ожидается 2000
  (сумма умножить на 10) делить на 100

FLANG_TYPE в файле given1.flang, строка 6, столбец 3: пример «опечатка в имени аргумента» функции «Скидка» не задаёт аргумент «сумма»
FLANG_UNKNOWN_NAME в файле given1.flang, строка 6, столбец 3: пример «опечатка в имени аргумента» функции «Скидка» задаёт неизвестный аргумент «сума»

FLANG_TYPE: a record field is not set. Records in flang have no gaps: an optional field is declared with the words иногда является.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «поле забыто»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  (покупка.«сумма» умножить на 10) делить на 100

FLANG_TYPE в файле rec1.flang, строка 10, столбец 3: пример «поле забыто»: аргумент «покупка»: не задано поле «постоянный клиент» записи «Покупка»

FLANG_TYPE: an example value outside its type.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «отрицательная сумма»
    дано сумма равно -5
    ожидается 0
  0

FLANG_TYPE в файле neg1.flang, строка 6, столбец 3: пример «отрицательная сумма»: аргумент «сумма»: -5 вне неотрицательное

An example with a negative amount is not needed for неотрицательное: such an input is rejected at the boundary, before the function.

Proof errors

FLANG_PRECONDITION_CALL — a call does not discharge a precondition. A требует condition is proved by the caller, and an unfit call is refused before running.

модуль «Скидка на вызове»

тотальная функция «Цена со скидкой»
  принимает цена: неотрицательное, скидка: неотрицательное
  возвращает число
  требует «скидка не больше цены» скидка не больше цена
  обеспечивает «цена не уходит в минус» результат не меньше 0
  цена минус скидка

тотальная функция «Цена товара по акции»
  возвращает число
  «Цена со скидкой» от 100 и 300

FLANG_PRECONDITION_CALL в файле pre1.flang, строка 12, столбец 3: вызов «Цена со скидкой» в функции «Цена товара по акции» не снимает предусловие «скидка не больше цены»: …

The message is long: after this the compiler lists which kinds of expressions it can bound and what is known at the call site. The first sentence is the one to read — it names the call and the condition. Fix: call от 1000 и 300, where the discount is not larger than the price. The limits of this check are narrow: a precondition written as a call to your own predicate function is never discharged, at any call site.

FLANG_PROOF_STEP — a theorem refers to a promise that does not exist.

модуль «Счёт»

тотальная функция «Позиций»
  принимает цены: список числа
  возвращает неотрицательное
  обеспечивает «позиций не меньше нуля» результат не меньше 0
  длина цены

тотальная функция «Вдвое»
  принимает цены: список числа
  возвращает число
  обеспечивает «вдвое не меньше нуля» результат не меньше 0
  («Позиций» от цены) умножить на 2

теорема «вдвое не меньше нуля»
  дано цены: список числа
  утверждаем результат не меньше 0
  по свойству «позиций больше нуля»
  следовательно доказано

FLANG_PROOF_STEP в файле proof1.flang, строка 18, столбец 3: шаг 1, теорема «вдвое не меньше нуля»: постусловия «позиций больше нуля» нет ни у одной функции модуля — сослаться не на что. к этому месту не известно ничего, кроме гипотез «дано»

Fix: по свойству «позиций не меньше нуля» — the promise name word for word.

FLANG_PROOF_CLAIM_MISMATCH — a theorem claims something other than what the function promises.

модуль «Счёт»

тотальная функция «Позиций»
  принимает цены: список числа
  возвращает неотрицательное
  обеспечивает «позиций не меньше нуля» результат не меньше 0
  длина цены

тотальная функция «Вдвое»
  принимает цены: список числа
  возвращает число
  обеспечивает «вдвое не меньше нуля» результат не меньше 0
  («Позиций» от цены) умножить на 2

теорема «вдвое не меньше нуля»
  дано цены: список числа
  утверждаем результат не меньше 1
  по свойству «позиций не меньше нуля»
  следовательно доказано

FLANG_PROOF_CLAIM_MISMATCH в файле proof2.flang, строка 17, столбец 3: теорема «вдвое не меньше нуля» утверждает не то, что обещает функция «Вдвое»: утверждение теоремы и постусловие обязаны совпадать слово в слово. Ядро не решает, что два разных утверждения означают одно и то же

Fix: утверждаем результат не меньше 0 — as in обеспечивает.

“Grid N” is not an error, but not a proof either. A promise the kernel did not derive is reported by flang check --proof like this:

  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 5 значений (примеры функции): … Это не доказательство — теоремы при утверждении нет

and the exit code is 3. With --strict the four outcomes get separate codes: 0 — everything proved, 1 — refuted, 3 — could not prove, 2 — not supported. The --fast flag skips the proof kernel and the examples and exits with code 4, so that the skip does not look green.

Fact errors

flang facts evaluates claims on JSON data. Code 1 here means not “broken” but “the claim does not hold”, and the verdict still arrives on stdout.

Refuted ("status": "refuted"). The data does not support the claim:

$ flang facts order-shipment.flang --facts order-shipment.blocked.facts.json --claims '["«Заказ с номером отгружается» от заказы, номер равно да"]'
"holds": false,
"why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». …",
"status": "refuted"

Refused ("status": "refused"). The claim is written wrong: the wrong number of arguments, or no such function.

"why": "функция «Заказ с номером отгружается» принимает 2 аргумент(ов), а в утверждении их 1"
"why": "функция «Отгрузить» не найдена в программе"

Arguments in a claim are separated by commas: от заказы, номер.

A malformed call — code 2:

$ flang facts order-shipment.flang --claims 'нет'
flang facts: --claims должен быть JSON-массивом строк

What the compiler does not catch

Three cases where the check is green while the reader expects a finding:

• a function without a возвращает line passes flang check with code 0 — the result type is inferred from the body. Write возвращает yourself: it is part of the contract, not decoration;
• a file without a first line модуль passes as “без имени модуля”, a module without a name;
• an unknown word in a condition (превышает) gives у 'если' нет ветки 'то' instead of “unknown comparison” — the column names the place of the error.

Sandbox practice

Change ожидается in any example and find FLANG_EXAMPLE in the answer. Then put the example back and change the cap in the promise «скидка ограничена» to 1000 — an example breaks, and the answer names FLANG_PROPERTY.

Delete the line случай «Разрешено» in «Причина отказа» and read FLANG_MATCH_NOT_EXHAUSTIVE. Then change the field заказ.«оплачен» to заказ.«оплата» and see which finding comes first.

Checklist: what to check when a model does not pass

1. The first line is модуль «Имя».
2. Read the first finding and its column; the others often follow from it.
3. FLANG_PARSE — indentation, the то and иначе branches, comparison words from the closed list.
4. FLANG_UNKNOWN_NAME — a typo in a type, function or argument name.
5. FLANG_TYPE — the field name, the result type, an ordering comparison on a non-number, all record fields in an example.
6. FLANG_MATCH_NOT_EXHAUSTIVE — every variant of the type is matched.
7. FLANG_NOT_TOTAL — recursion moves towards a smaller value.
8. FLANG_EXAMPLE — first decide who is right: the example or the rule.
9. Code 3 from flang check --proof — read which promises rest on examples only and decide whether to accept that.

Catalog cases on this topic