Руководство по Ada (Ada 2022)
J.15.2 Предикат No_Return
Синтаксис
Форма предиката pragma No_Return, являющегося предикатом представления (см. 13.1), имеет следующий вид:
pragma No_Return (имя_подпрограммы_локальное_имя{, имя_подпрограммы_локальное_имя});
Правила легальности
Каждое имя_подпрограммы_локальное_имя должно обозначать одну или несколько подпрограмм или обобщённых подпрограмм. Имя_подпрограммы_локальное_имя не должно обозначать пустую процедуру или экземпляр обобщённого блока.
Статическая семантика
Предикат No_Return указывает, что аспект No_Return (см. 6.5.1) для каждой подпрограммы, обозначенной каждым локальное_имя, заданным в pragma, имеет значение True.
