При двукратном анализе целого числа из одной и той же строки GNATprove не допускает, чтобы одно и то же целое число производилось дважды. Как мне это исправить?
Основной файл:
with String_Problem;
procedure Eq_Test is
begin
String_Problem.String_Equal("4456");
end Eq_Test;
String_Problem.ads:
package String_Problem
with Spark_Mode
is
procedure String_Equal
(A : String)
with
Ghost;
end String_Problem;
String_Problem.adb:
package body String_Problem
with Spark_Mode
is
procedure String_Equal
(A : String)
is
X1 : Integer;
X2 : Integer;
begin
X1 := Integer'Value (A);
pragma Annotate
(Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
X2 := Integer'Value (A);
pragma Annotate
(Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
pragma Assert (X1 = X2);
end String_Equal;
end String_Problem;
Выход GNATProve:
alr gnatprove
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
string_problem.adb:16:22: medium: assertion might fail
16 | pragma Assert (X1 = X2);
| ^~~~~~~
Summary logged in [path]/gnatprove/gnatprove.out
@JimRogers Боюсь, я не понимаю, что ты имеешь в виду
Доказали ли компиляторы AdaCore атрибут «Value»? GnatProve может быть не в состоянии определить, что значение всегда возвращает один и тот же результат для согласованного значения параметра.
Ах, я только что забрал Ada/SPARK, и поэтому понятия не имею, как это узнать!
Конечно, SPARK может доказать следующее: X1 := Integer'Value(A); Х2 := Х1; прагма Assert (X1 = X2);
Возможно, пока нет приемлемого ответа.
Есть очень похожий вопрос: Ada SPARK преобразовать строку в целое число
Обычно GNATProve может проверять такие вещи. Следующий код обычно не вызывает проблем:
X1 := function_1(A)
X2 := function_1(A)
pragma Assert (X1 = X2)
Это возможно даже для GNATProve, если функция_1 не может быть проверена или если функция_1 имеет открытые проблемы или даже не реализована. GNATProve должен знать только поток данных функции_1. Для функций это понятно. SPARK (не Ada) требует, чтобы функции не имели побочных эффектов. Зная это, становится очевидным, что два вызова дают один и тот же результат. И это также ясно для GNATProve.
Но у тебя нет функций. У вас есть атрибут Value. И, как показывает другой вопрос, у GNATProve есть ограничения, когда дело доходит до атрибута Value. Похоже, что GNATProve не использует тот факт, что его двойной вызов дает один и тот же результат. GNATProve, похоже, отказывается включать какие-либо сведения об атрибуте value.
Поскольку это ограничение, вы ничего не сможете с этим поделать.
Либо вы ставите pragma Assume(X1 = X2);
, либо пишете функцию вокруг атрибута Value. Если это вариант для вас, ваш код будет таким:
package body Show_Runtime_Errors is
function Integer_Value(A : in String) return Integer is
(Integer'Value(A));
pragma Annotate(Gnatprove, False_Positive, "precondition might fail", "GNATProve limitation");
procedure String_Equal
(A : String)
is
X1 : Integer;
X2 : Integer;
begin
X1 := Integer_Value (A);
X2 := Integer_Value (A);
pragma Assert (X1 = X2);
end String_Equal;
end Show_Runtime_Errors;
Атрибут «Значение» был подтвержден в SPARK?