procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

ada: Add annotations for proof of termination of runtime units

Browse source 
String-manipulating functions should always terminate. Add justification
for the termination of Mapping function parameter, and loop variants
where needed. This is needed for GNATprove to prove termination.

gcc/ada/

	* libgnat/a-strbou.ads: Add justifications for Mapping.
	* libgnat/a-strfix.adb: Same.
	* libgnat/a-strfix.ads: Same.
	* libgnat/a-strsea.adb: Same.
	* libgnat/a-strsea.ads: Same.
	* libgnat/a-strsup.adb: Same and add loop variants.
	* libgnat/a-strsup.ads: Same and add specification of termination.
This commit is contained in:
Yannick Moy 2023-01-16 11:33:03 +00:00 • committed by Marc Poulhiès
parent a398b5479c
commit 9c213cb867
7 changed files with 66 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
gcc/ada/libgnat/a-strbou.ads
View file

@ -1341,6 +1341,9 @@ package Ada.Strings.Bounded with SPARK_Mode is
(for all K in 1 .. Length (Source) =>
Element (Translate'Result, K) = Mapping (Element (Source, K))),
Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
procedure Translate
(Source : in out Bounded_String;
@ -1352,6 +1355,9 @@ package Ada.Strings.Bounded with SPARK_Mode is
(for all K in 1 .. Length (Source) =>
Element (Source, K) = Mapping (Element (Source'Old, K))),
Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
---------------------------------------
-- String Transformation Subprograms --

12
gcc/ada/libgnat/a-strfix.adb
View file

@ -773,12 +773,18 @@ package body Ada.Strings.Fixed with SPARK_Mode is
do
for J in Source'Range loop
Result (J - (Source'First - 1)) := Mapping.all (Source (J));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Loop_Invariant
(for all K in Source'First .. J =>
Result (K - (Source'First - 1))'Initialized);
pragma Loop_Invariant
(for all K in Source'First .. J =>
Result (K - (Source'First - 1)) = Mapping (Source (K)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
end return;
end Translate;
@ -791,9 +797,15 @@ package body Ada.Strings.Fixed with SPARK_Mode is
begin
for J in Source'Range loop
Source (J) := Mapping.all (Source (J));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Loop_Invariant
(for all K in Source'First .. J =>
Source (K) = Mapping (Source'Loop_Entry (K)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
end Translate;

6
gcc/ada/libgnat/a-strfix.ads
View file

@ -754,6 +754,9 @@ package Ada.Strings.Fixed with SPARK_Mode is
= Mapping (Source (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
function Translate
(Source : String;
@ -796,6 +799,9 @@ package Ada.Strings.Fixed with SPARK_Mode is
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
procedure Translate
(Source : in out String;

18
gcc/ada/libgnat/a-strsea.adb
View file

@ -185,6 +185,9 @@ package body Ada.Strings.Search with SPARK_Mode is
Ind := Ind + 1;
for K in Pattern'Range loop
if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
goto Cont;
end if;
@ -192,6 +195,9 @@ package body Ada.Strings.Search with SPARK_Mode is
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
pragma Assert (Match (Source, Pattern, Mapping, Ind));
@ -489,12 +495,18 @@ package body Ada.Strings.Search with SPARK_Mode is
if Pattern (K) /= Mapping.all
(Source (Ind + (K - Pattern'First)))
then
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
goto Cont1;
end if;
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
pragma Assert (Match (Source, Pattern, Mapping, Ind));
@ -515,12 +527,18 @@ package body Ada.Strings.Search with SPARK_Mode is
if Pattern (K) /= Mapping.all
(Source (Ind + (K - Pattern'First)))
then
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
goto Cont2;
end if;
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
return Ind;

3
gcc/ada/libgnat/a-strsea.ads
View file

@ -74,6 +74,9 @@ package Ada.Strings.Search with SPARK_Mode is
and then Source'Length > 0
and then From in Source'First .. Source'Last - (Pattern'Length - 1),
Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
function Match
(Source : String;

14
gcc/ada/libgnat/a-strsup.adb
View file

@ -1570,6 +1570,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
(for all K in 1 .. Indx =>
Result.Data (K) =
Item (Item'First + (K - 1) mod Ilen));
pragma Loop_Variant (Increases => Indx);
end loop;
Result.Data (Indx + 1 .. Max_Length) := Super_String_Data
@ -1609,6 +1610,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
(for all K in Indx + 1 .. Max_Length =>
Result.Data (K) =
Item (Item'Last - (Max_Length - K) mod Ilen));
pragma Loop_Variant (Decreases => Indx);
end loop;
Result.Data (1 .. Indx) :=
@ -1845,10 +1847,16 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
begin
for J in 1 .. Source.Current_Length loop
Result.Data (J) := Mapping.all (Source.Data (J));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
pragma Loop_Invariant
(for all K in 1 .. J =>
Result.Data (K) = Mapping (Source.Data (K)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
Result.Current_Length := Source.Current_Length;
@ -1862,9 +1870,15 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
begin
for J in 1 .. Source.Current_Length loop
Source.Data (J) := Mapping.all (Source.Data (J));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Loop_Invariant
(for all K in 1 .. J =>
Source.Data (K) = Mapping (Source'Loop_Entry.Data (K)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
end Super_Translate;

7
gcc/ada/libgnat/a-strsup.ads
View file

@ -53,6 +53,7 @@ with Ada.Strings.Text_Buffers;
package Ada.Strings.Superbounded with SPARK_Mode is
pragma Preelaborate;
pragma Annotate (GNATprove, Always_Return, Superbounded);
-- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
-- derived from Super_String, with the constraint of the maximum length.
@ -1406,6 +1407,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is
Super_Element (Super_Translate'Result, K) =
Mapping (Super_Element (Source, K))),
Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
procedure Super_Translate
(Source : in out Super_String;
@ -1418,6 +1422,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is
Super_Element (Source, K) =
Mapping (Super_Element (Source'Old, K))),
Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
---------------------------------------
-- String Transformation Subprograms --