Нет глобального контракта для процедуры/функции

Это означает, что анализатор не может «увидеть», могут ли быть затронуты глобальные переменные при вызове этой функции. Поэтому предполагается, что этот вызов ничего не изменяет (иначе все другие доказательства могут быть немедленно опровергнуты). Вероятно, это правильное предположение для вашего конкретного примера, но оно может оказаться недействительным во встроенной системе, где пользовательская реализация Put_Line может делать что угодно.

Есть два способа передать недостающую информацию:

1. верификатор может проверить исходный код функции. Затем он может попытаться сам сгенерировать глобальные контракты.
2. глобальные контракты указаны явно, см. RM 6.1.4 (http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#global-aspects)

В этом случае вызываемая вами процедура является частью системы времени выполнения (RTS), и поэтому источник не виден, и вы, вероятно, не можете/не должны его изменять.

Что делать на практике?

Подавление предупреждений почти никогда не является хорошей идеей, особенно когда вы работаете над чем-то важным для безопасности. Обычно код нужно менять до тех пор, пока предупреждение не исчезнет, ​​или должен начаться какой-то процесс обоснования.

Если вы серьезно относитесь к результатам анализа, я рекомендую не использовать такие подпрограммы. Если вам действительно нужен вывод туда, либо напишите свою собственную процедуру, заменяющую подпрограмму RTS, либо убедитесь, что подпрограмма действительно не имеет побочных эффектов. Это также подтверждается тем, на что ссылается Фредерик: даже если вызываемый объект не имеет побочных эффектов, вы не знаете, вызывает ли он исключение для определенных входных данных (например, очень длинных строк).

Если вы не так серьезно относитесь к результатам, вы можете рассматривать этот конкретный результат как предупреждение, с которым вы можете жить.

Пакеты-оболочки для использования при разработке приложений SPARK можно найти здесь: https://github.com/joakim-strandberg/aida_2012

Я думаю, что вы просто не можете добавлять контракты Spark к коду, которым вы не владеете, особенно к коду из стандарта Ada.

Что касается Text_Io, я нашел что-то, что может быть полезно для вас в справочном руководстве.

ИЗМЕНИТЬ

Другое решение по сравнению с тем, что сказал Мартин, согласно Книга "Создание приложений с высокой целостностью с помощью Spark" состоит в создании пакета-оболочки.

Поскольку Spark требует, чтобы вы работали с пакетами Spark, но позволяет вам зависеть от спецификации Spark с телом Ada, решение состоит в том, чтобы создать пакет Spark, обертывающий ваши вызовы Ada.Text_io.

Это может быть утомительно, так как вам придется оборачивать возможные исключения, возможно, определять определенные типы и т. д., но таким образом вы сможете выполнять VC в своем полном пакете Spark.