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

Для критичных систем стандарты запрещают динамическую память вообще

Отвечая на вопрос «что за гарантии по памяти для кода ракет»: ответ оказался не тем, которого ждали.

MISRA C Dir 4.12 и Rule 21.3 — обе Required, и рабочая группа MISRA прямо закрыла лазейку: запрет распространяется «also to any user-defined equivalent functions». То есть свою арену тоже нельзя.

Практика отрасли: выделить при старте и никогда не освобождать (JSF++ AV 206, Power of 10 правило 3, JPL правило 5, NASA F Prime).

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

Такой режим выразим: в языке уже есть два объявляемых предела того же вида, а замер показал, что 42,2 % корпуса (1236 функций из 2930) уже получают оценку сверху многочленом. Не хватает предела на размер входа, сильной оценки размера выделяемого и зеркала анализа в самоприменённой части. Оценка: ~2300–3700 строк, форма — пометка на функции, как тотальная.

Важное предупреждение: пометка тотальная памяти не ограничивает — ровно как total в Idris и Agda. Завершаемость и ограниченность памяти — разные свойства.

Связано: memory-per-category-is-regions, arena-never-releases