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