How do I convince GNATprove that calling Integer'Value on the same input twice should produce the same result?
When parsing an integer from the same string twice, GNATprove doesn't accept that the same integer should be produced twice. How should I rectify this?
Main file:
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 output:
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