From dcedb463e99fa38ca330f4a2e651d13640bb6657 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Fri, 19 Aug 2022 10:56:30 +0200 Subject: [PATCH] Add `Always_Return` annotations Ref. #1131 --- rflx/templates/rflx_arithmetic.ads | 4 +++- rflx/templates/rflx_builtin_types-conversions.ads | 4 +++- rflx/templates/rflx_builtin_types.ads | 4 +++- rflx/templates/rflx_generic_types.ads | 4 +++- rflx/templates/rflx_message_sequence.ads | 4 +++- rflx/templates/rflx_scalar_sequence.ads | 4 +++- tests/integration/shared/generated/rflx-rflx_arithmetic.ads | 4 +++- .../shared/generated/rflx-rflx_builtin_types-conversions.ads | 4 +++- .../integration/shared/generated/rflx-rflx_builtin_types.ads | 4 +++- .../integration/shared/generated/rflx-rflx_generic_types.ads | 4 +++- .../shared/generated/rflx-rflx_message_sequence.ads | 4 +++- .../shared/generated/rflx-rflx_scalar_sequence.ads | 4 +++- tests/spark/generated/rflx-rflx_arithmetic.ads | 4 +++- tests/spark/generated/rflx-rflx_builtin_types-conversions.ads | 4 +++- tests/spark/generated/rflx-rflx_builtin_types.ads | 4 +++- tests/spark/generated/rflx-rflx_generic_types.ads | 4 +++- tests/spark/generated/rflx-rflx_message_sequence.ads | 4 +++- tests/spark/generated/rflx-rflx_scalar_sequence.ads | 4 +++- 18 files changed, 54 insertions(+), 18 deletions(-) diff --git a/rflx/templates/rflx_arithmetic.ads b/rflx/templates/rflx_arithmetic.ads index f85ead8b17..d2685e9ebb 100644 --- a/rflx/templates/rflx_arithmetic.ads +++ b/rflx/templates/rflx_arithmetic.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package {prefix}RFLX_Arithmetic with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type U64 is mod 2**64 with diff --git a/rflx/templates/rflx_builtin_types-conversions.ads b/rflx/templates/rflx_builtin_types-conversions.ads index a1957c0ccc..01574e01dd 100644 --- a/rflx/templates/rflx_builtin_types-conversions.ads +++ b/rflx/templates/rflx_builtin_types-conversions.ads @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); with {prefix}RFLX_Arithmetic; package {prefix}RFLX_Builtin_Types.Conversions with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, Conversions); diff --git a/rflx/templates/rflx_builtin_types.ads b/rflx/templates/rflx_builtin_types.ads index a7a0ea055f..f7a1cac3f3 100644 --- a/rflx/templates/rflx_builtin_types.ads +++ b/rflx/templates/rflx_builtin_types.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package {prefix}RFLX_Builtin_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type Length is new Natural; diff --git a/rflx/templates/rflx_generic_types.ads b/rflx/templates/rflx_generic_types.ads index c0894f59f3..a98da9d6fb 100644 --- a/rflx/templates/rflx_generic_types.ads +++ b/rflx/templates/rflx_generic_types.ads @@ -11,7 +11,9 @@ generic type Custom_Length is range <>; type Custom_Bit_Length is range <>; package {prefix}RFLX_Generic_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is subtype Index is Custom_Index; diff --git a/rflx/templates/rflx_message_sequence.ads b/rflx/templates/rflx_message_sequence.ads index 1c0b370aa5..806e9bef5f 100644 --- a/rflx/templates/rflx_message_sequence.ads +++ b/rflx/templates/rflx_message_sequence.ads @@ -12,7 +12,9 @@ generic with function Element_Initialized (Ctx : Element_Context) return Boolean; with function Element_Valid_Message (Ctx : Element_Context) return Boolean; package {prefix}RFLX_Message_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence); diff --git a/rflx/templates/rflx_scalar_sequence.ads b/rflx/templates/rflx_scalar_sequence.ads index cf2d9380c2..74a5722def 100644 --- a/rflx/templates/rflx_scalar_sequence.ads +++ b/rflx/templates/rflx_scalar_sequence.ads @@ -8,7 +8,9 @@ generic with function To_Actual (Element : {prefix}RFLX_Types.Base_Integer) return Element_Type; with function To_Base_Int (Element : Element_Type) return {prefix}RFLX_Types.Base_Integer; package {prefix}RFLX_Scalar_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence); diff --git a/tests/integration/shared/generated/rflx-rflx_arithmetic.ads b/tests/integration/shared/generated/rflx-rflx_arithmetic.ads index a56c404343..c1f00ed97b 100644 --- a/tests/integration/shared/generated/rflx-rflx_arithmetic.ads +++ b/tests/integration/shared/generated/rflx-rflx_arithmetic.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package RFLX.RFLX_Arithmetic with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type U64 is mod 2**64 with diff --git a/tests/integration/shared/generated/rflx-rflx_builtin_types-conversions.ads b/tests/integration/shared/generated/rflx-rflx_builtin_types-conversions.ads index 73023906fb..1040f49d3d 100644 --- a/tests/integration/shared/generated/rflx-rflx_builtin_types-conversions.ads +++ b/tests/integration/shared/generated/rflx-rflx_builtin_types-conversions.ads @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); with RFLX.RFLX_Arithmetic; package RFLX.RFLX_Builtin_Types.Conversions with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, Conversions); diff --git a/tests/integration/shared/generated/rflx-rflx_builtin_types.ads b/tests/integration/shared/generated/rflx-rflx_builtin_types.ads index 52dc6a1b36..7e162d6bea 100644 --- a/tests/integration/shared/generated/rflx-rflx_builtin_types.ads +++ b/tests/integration/shared/generated/rflx-rflx_builtin_types.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package RFLX.RFLX_Builtin_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type Length is new Natural; diff --git a/tests/integration/shared/generated/rflx-rflx_generic_types.ads b/tests/integration/shared/generated/rflx-rflx_generic_types.ads index e78038b117..3a34403a8e 100644 --- a/tests/integration/shared/generated/rflx-rflx_generic_types.ads +++ b/tests/integration/shared/generated/rflx-rflx_generic_types.ads @@ -11,7 +11,9 @@ generic type Custom_Length is range <>; type Custom_Bit_Length is range <>; package RFLX.RFLX_Generic_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is subtype Index is Custom_Index; diff --git a/tests/integration/shared/generated/rflx-rflx_message_sequence.ads b/tests/integration/shared/generated/rflx-rflx_message_sequence.ads index 2452ba3d3d..38216afcb0 100644 --- a/tests/integration/shared/generated/rflx-rflx_message_sequence.ads +++ b/tests/integration/shared/generated/rflx-rflx_message_sequence.ads @@ -12,7 +12,9 @@ generic with function Element_Initialized (Ctx : Element_Context) return Boolean; with function Element_Valid_Message (Ctx : Element_Context) return Boolean; package RFLX.RFLX_Message_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence); diff --git a/tests/integration/shared/generated/rflx-rflx_scalar_sequence.ads b/tests/integration/shared/generated/rflx-rflx_scalar_sequence.ads index 645d763243..f6d5ec9d3d 100644 --- a/tests/integration/shared/generated/rflx-rflx_scalar_sequence.ads +++ b/tests/integration/shared/generated/rflx-rflx_scalar_sequence.ads @@ -8,7 +8,9 @@ generic with function To_Actual (Element : RFLX.RFLX_Types.Base_Integer) return Element_Type; with function To_Base_Int (Element : Element_Type) return RFLX.RFLX_Types.Base_Integer; package RFLX.RFLX_Scalar_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence); diff --git a/tests/spark/generated/rflx-rflx_arithmetic.ads b/tests/spark/generated/rflx-rflx_arithmetic.ads index a56c404343..c1f00ed97b 100644 --- a/tests/spark/generated/rflx-rflx_arithmetic.ads +++ b/tests/spark/generated/rflx-rflx_arithmetic.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package RFLX.RFLX_Arithmetic with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type U64 is mod 2**64 with diff --git a/tests/spark/generated/rflx-rflx_builtin_types-conversions.ads b/tests/spark/generated/rflx-rflx_builtin_types-conversions.ads index 73023906fb..1040f49d3d 100644 --- a/tests/spark/generated/rflx-rflx_builtin_types-conversions.ads +++ b/tests/spark/generated/rflx-rflx_builtin_types-conversions.ads @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); with RFLX.RFLX_Arithmetic; package RFLX.RFLX_Builtin_Types.Conversions with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, Conversions); diff --git a/tests/spark/generated/rflx-rflx_builtin_types.ads b/tests/spark/generated/rflx-rflx_builtin_types.ads index 52dc6a1b36..7e162d6bea 100644 --- a/tests/spark/generated/rflx-rflx_builtin_types.ads +++ b/tests/spark/generated/rflx-rflx_builtin_types.ads @@ -1,7 +1,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); package RFLX.RFLX_Builtin_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is type Length is new Natural; diff --git a/tests/spark/generated/rflx-rflx_generic_types.ads b/tests/spark/generated/rflx-rflx_generic_types.ads index e78038b117..3a34403a8e 100644 --- a/tests/spark/generated/rflx-rflx_generic_types.ads +++ b/tests/spark/generated/rflx-rflx_generic_types.ads @@ -11,7 +11,9 @@ generic type Custom_Length is range <>; type Custom_Bit_Length is range <>; package RFLX.RFLX_Generic_Types with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is subtype Index is Custom_Index; diff --git a/tests/spark/generated/rflx-rflx_message_sequence.ads b/tests/spark/generated/rflx-rflx_message_sequence.ads index 2452ba3d3d..38216afcb0 100644 --- a/tests/spark/generated/rflx-rflx_message_sequence.ads +++ b/tests/spark/generated/rflx-rflx_message_sequence.ads @@ -12,7 +12,9 @@ generic with function Element_Initialized (Ctx : Element_Context) return Boolean; with function Element_Valid_Message (Ctx : Element_Context) return Boolean; package RFLX.RFLX_Message_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence); diff --git a/tests/spark/generated/rflx-rflx_scalar_sequence.ads b/tests/spark/generated/rflx-rflx_scalar_sequence.ads index 645d763243..f6d5ec9d3d 100644 --- a/tests/spark/generated/rflx-rflx_scalar_sequence.ads +++ b/tests/spark/generated/rflx-rflx_scalar_sequence.ads @@ -8,7 +8,9 @@ generic with function To_Actual (Element : RFLX.RFLX_Types.Base_Integer) return Element_Type; with function To_Base_Int (Element : Element_Type) return RFLX.RFLX_Types.Base_Integer; package RFLX.RFLX_Scalar_Sequence with - SPARK_Mode + SPARK_Mode, + Annotate => + (GNATprove, Always_Return) is pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence);