How do I convince GNATprove that calling Integer'Value on the same input twice should produce the same result?
8 November 2022 at 15:03
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