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

Solution

There may be no acceptable answer yet.

There is a very similar question: Ada SPARK convert string to integer

Normally GNATProve can verify such things. The following code is normally no problem:

X1 := function_1(A)
X2 := function_1(A)
pragma Assert (X1 = X2)

This is even possible for GNATProve if function_1 cannot be verified or if function_1 has open issues or is not even implemented. GNATProve only has to know the data flow of function_1. For functions this is clear. SPARK (not Ada) requires that functions have no side effects. When knowing this, then it is obvious that two calls produce the same result. And this is also clear for GNATProve.

But you have no functions. You have the Value attribute. And as the other question indicates, there are limitations with GNATProve when it comes to the Value attribute. It looks like GNATProve does not use the fact that calling it twice produces the same result. GNATProve seems to refuse to incorporate any knowledge of the value attribute.

As it is a limitation there will be nothing you can do against it.

Either you place an pragma Assume(X1 = X2); or you write a function around the Value attribute. If this is an option for you, your code will be this:

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;